1  /-
  2  Copyright (c) 2018 Patrick Massot. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Authors: Patrick Massot, Johannes Hölzl
  5  
  6  Uniform structure on topological groups:
  7  
  8  * `topological_add_group.to_uniform_space` and `topological_add_group_is_uniform` can be used to
  9    construct a canonical uniformity for a topological add group.
 10  
 11  * extension of ℤ-bilinear maps to complete groups (useful for ring completions)
 12  
 13  * `add_group_with_zero_nhd`: construct the topological structure from a group with a neighbourhood
 14    around zero. Then with `topological_add_group.to_uniform_space` one can derive a `uniform_space`.
 15  -/
 16  import topology.uniform_space.uniform_embedding topology.uniform_space.complete_separated
src         └──────────────────────────────────────┘ └───────────────────────────────────────┘
 17  import topology.algebra.group
src         └────────────────────┘
 18  
 19  noncomputable theory
 20  open_locale classical uniformity topological_space
 21  
 22  section uniform_add_group
 23  open filter set
 24  
 25  variables {α : Type*} {β : Type*}
 26  
 27  /-- A uniform (additive) group is a group in which the addition and negation are
 28    uniformly continuous. -/
 29  class uniform_add_group (α : Type*) [uniform_space α] [add_group α] : Prop :=
id                                └───┘   └───────────┘    └───────┘ 
src                                       └───────────┘     └───────┘
typ                               └───┘   └───────────┘    └───────┘ 
doc                                       └───────────┘
 30  (uniform_continuous_sub : uniform_continuous (λp:α×α, p.1 - p.2))
id                             └────────────────┘          
src                            └────────────────┘              
typ                            └────────────────┘          
 31  
 32  theorem uniform_add_group.mk' {α} [uniform_space α] [add_group α]
id                                      └───────────┘    └───────┘ 
src                                     └───────────┘     └───────┘
typ                                     └───────────┘    └───────┘ 
doc                                     └───────────┘
 33    (h₁ : uniform_continuous (λp:α×α, p.1 + p.2))
id           └────────────────┘          
src          └────────────────┘              
typ          └────────────────┘          
 34    (h₂ : uniform_continuous (λp:α, -p)) : uniform_add_group α :=
id           └────────────────┘            └───────────────┘ 
src          └────────────────┘              └───────────────┘
typ          └────────────────┘            └───────────────┘ 
doc                                           └───────────────┘
 35  ⟨h₁.comp (uniform_continuous_fst.prod_mk (h₂.comp uniform_continuous_snd))⟩
id    └┘└───┘  └────────────────────┘└──────┘  └┘└───┘ └────────────────────┘
src     └───┘  └────────────────────┘└──────┘    └───┘ └────────────────────┘
typ   └┘└───┘  └────────────────────┘└──────┘  └┘└───┘ └────────────────────┘
 36  
 37  variables [uniform_space α] [add_group α] [uniform_add_group α]
id              └───────────┘    └───────┘     └───────────────┘
src             └───────────┘     └───────┘     └───────────────┘
typ             └───────────┘    └───────┘     └───────────────┘
doc             └───────────┘                   └───────────────┘
 38  
 39  lemma uniform_continuous_sub : uniform_continuous (λp:α×α, p.1 - p.2) :=
id                                  └────────────────┘          
src                                 └────────────────┘              
typ                                 └────────────────┘          
 40  uniform_add_group.uniform_continuous_sub α
id   └──────────────────────────────────────┘ 
src  └──────────────────────────────────────┘
typ  └──────────────────────────────────────┘ 
 41  
 42  lemma uniform_continuous.sub [uniform_space β] {f : β → α} {g : β → α}
id                                 └───────────┘                     
src                                └───────────┘
typ                                └───────────┘                     
doc                                └───────────┘
 43    (hf : uniform_continuous f) (hg : uniform_continuous g) : uniform_continuous (λx, f x - g x) :=
id           └────────────────┘         └────────────────┘     └────────────────┘         
src          └────────────────┘          └────────────────┘      └────────────────┘          
typ          └────────────────┘         └────────────────┘     └────────────────┘         
 44  uniform_continuous_sub.comp (hf.prod_mk hg)
id   └────────────────────┘└───┘  └┘└──────┘ └┘
src  └────────────────────┘└───┘    └──────┘
typ  └────────────────────┘└───┘  └┘└──────┘ └┘
 45  
 46  lemma uniform_continuous.neg [uniform_space β] {f : β → α}
id                                 └───────────┘           
src                                └───────────┘
typ                                └───────────┘           
doc                                └───────────┘
 47    (hf : uniform_continuous f) : uniform_continuous (λx, - f x) :=
id           └────────────────┘     └────────────────┘       
src          └────────────────┘      └────────────────┘      
typ          └────────────────┘     └────────────────┘       
 48  have uniform_continuous (λx, 0 - f x),
id        └────────────────┘         
src       └────────────────┘        
typ       └────────────────┘         
 49    from uniform_continuous_const.sub hf,
id          └──────────────────────┘└──┘ └┘
src         └──────────────────────┘└──┘
typ         └──────────────────────┘└──┘ └┘
 50  by simp * at *
src     └───────────
typ     └───────────
doc     └───────────
txt     └───────────
par     └───────────
pid         └──┘
st     └────────────
 51  
src  
typ  
doc  
txt  
par  
pid  
st   
 52  lemma uniform_continuous_neg : uniform_continuous (λx:α, - x) :=
id                                  └────────────────┘        
src                                 └────────────────┘        
typ                                 └────────────────┘        
 53  uniform_continuous_id.neg
id   └───────────────────┘└──┘
src  └───────────────────┘└──┘
typ  └───────────────────┘└──┘
 54  
 55  lemma uniform_continuous.add [uniform_space β] {f : β → α} {g : β → α}
id                                 └───────────┘                     
src                                └───────────┘
typ                                └───────────┘                     
doc                                └───────────┘
 56    (hf : uniform_continuous f) (hg : uniform_continuous g) : uniform_continuous (λx, f x + g x) :=
id           └────────────────┘         └────────────────┘     └────────────────┘         
src          └────────────────┘          └────────────────┘      └────────────────┘          
typ          └────────────────┘         └────────────────┘     └────────────────┘         
 57  have uniform_continuous (λx, f x - - g x), from hf.sub hg.neg,
id        └────────────────┘                  └┘└──┘ └┘└──┘
src       └────────────────┘                         └──┘   └──┘
typ       └────────────────┘                  └┘└──┘ └┘└──┘
 58  by simp * at *
src     └───────────
typ     └───────────
doc     └───────────
txt     └───────────
par     └───────────
pid         └──┘
st     └────────────
 59  
src  
typ  
doc  
txt  
par  
pid  
st   
 60  lemma uniform_continuous_add : uniform_continuous (λp:α×α, p.1 + p.2) :=
id                                  └────────────────┘          
src                                 └────────────────┘              
typ                                 └────────────────┘          
 61  uniform_continuous_fst.add uniform_continuous_snd
id   └────────────────────┘└──┘ └────────────────────┘
src  └────────────────────┘└──┘ └────────────────────┘
typ  └────────────────────┘└──┘ └────────────────────┘
 62  
 63  @[priority 10]
 64  instance uniform_add_group.to_topological_add_group : topological_add_group α :=
id                                                         └───────────────────┘ 
src                                                        └───────────────────┘
typ                                                        └───────────────────┘ 
doc                                                        └───────────────────┘
 65  { continuous_add := uniform_continuous_add.continuous,
id                       └────────────────────┘└─────────┘
src                      └────────────────────┘└─────────┘
typ                      └────────────────────┘└─────────┘
 66    continuous_neg := uniform_continuous_neg.continuous }
id                       └────────────────────┘└─────────┘
src                      └────────────────────┘└─────────┘
typ                      └────────────────────┘└─────────┘
 67  
 68  instance [uniform_space β] [add_group β] [uniform_add_group β] : uniform_add_group (α × β) :=
id             └───────────┘    └───────┘    └───────────────┘     └───────────────┘    
src            └───────────┘     └───────┘     └───────────────┘      └───────────────┘    
typ            └───────────┘    └───────┘    └───────────────┘     └───────────────┘    
doc            └───────────┘                   └───────────────┘      └───────────────┘
 69  ⟨((uniform_continuous_fst.comp uniform_continuous_fst).sub
id      └────────────────────┘└───┘ └────────────────────┘ └─┘
src     └────────────────────┘└───┘ └────────────────────┘ └─┘
typ     └────────────────────┘└───┘ └────────────────────┘ └─┘
 70    (uniform_continuous_fst.comp uniform_continuous_snd)).prod_mk
id      └────────────────────┘└───┘ └────────────────────┘  └─────┘
src     └────────────────────┘└───┘ └────────────────────┘  └─────┘
typ     └────────────────────┘└───┘ └────────────────────┘  └─────┘
 71   ((uniform_continuous_snd.comp uniform_continuous_fst).sub
id      └────────────────────┘└───┘ └────────────────────┘ └─┘
src     └────────────────────┘└───┘ └────────────────────┘ └─┘
typ     └────────────────────┘└───┘ └────────────────────┘ └─┘
 72    (uniform_continuous_snd.comp uniform_continuous_snd))⟩
id      └────────────────────┘└───┘ └────────────────────┘
src     └────────────────────┘└───┘ └────────────────────┘
typ     └────────────────────┘└───┘ └────────────────────┘
 73  
 74  lemma uniformity_translate (a : α) : (𝓤 α).map (λx:α×α, (x.1 + a, x.2 + a)) = 𝓤 α :=
id                                          └─┘                     
src                                           └─┘                          
typ                                         └─┘                     
doc                                           └─┘                                 
 75  le_antisymm
id   └─────────┘
src  └─────────┘
typ  └─────────┘
 76    (uniform_continuous_id.add uniform_continuous_const)
id      └───────────────────┘└──┘ └──────────────────────┘
src     └───────────────────┘└──┘ └──────────────────────┘
typ     └───────────────────┘└──┘ └──────────────────────┘
 77    (calc 𝓤 α =
id            
src          
typ           
doc          
 78      ((𝓤 α).map (λx:α×α, (x.1 + -a, x.2 + -a))).map (λx:α×α, (x.1 + a, x.2 + a)) :
id           └─┘                   └─┘                
src           └─┘                         └─┘                    
typ          └─┘                   └─┘                
doc           └─┘                                 └─┘
 79        by simp [filter.map_map, (∘)]; exact filter.map_id.symm
id                  └────────────┘             └────────────────┘
src           └────┘└────────────┘└┘└─┘  └────┘└────────────────┘
typ           └────┘└────────────┘└┘└─┘  └────┘└────────────────┘
doc           └────┘              └┘ └─┘  └────┘                  
txt           └────┘              └┘ └─┘  └────┘                  
par           └────┘              └┘ └─┘  └────┘                  
pid                             └┘ └─┘                         
st           └─────────────────────────────────────────────────────
 80      ... ≤ (𝓤 α).map (λx:α×α, (x.1 + a, x.2 + a)) :
id                └─┘                
src  ───┘          └─┘                    
typ  ───┘         └─┘                
doc  ───┘          └─┘
txt  ───┘
par  ───┘
pid  ───┘
st   ───┘
 81        filter.map_mono (uniform_continuous_id.add uniform_continuous_const))
id         └─────────────┘  └───────────────────┘└──┘ └──────────────────────┘
src        └─────────────┘  └───────────────────┘└──┘ └──────────────────────┘
typ        └─────────────┘  └───────────────────┘└──┘ └──────────────────────┘
 82  
 83  lemma uniform_embedding_translate (a : α) : uniform_embedding (λx:α, x + a) :=
id                                              └───────────────┘         
src                                              └───────────────┘          
typ                                             └───────────────┘         
 84  { comap_uniformity := begin
st                         └─────
 85      rw [← uniformity_translate a, comap_map] {occs := occurrences.pos [1]},
id             └──────────────────┘   └───────┘           └─────────────┘  
src      └────┘└──────────────────┘ └┘└───────┘└┘ └──────┘└─────────────┘
typ      └────┘└──────────────────┘└┘└───────┘└┘ └──────┘└─────────────┘
doc      └────┘                     └┘         └┘ └──────┘                 
txt      └────┘                     └┘         └┘ └──────┘                 
par      └────┘                     └┘         └┘ └──────┘                 
pid        └──┘                     └┘          └──────┘                 
st   ───────────────────────────────┘└─────────┘└────────────────────────────┘└─
 86      rintros ⟨p₁, p₂⟩ ⟨q₁, q₂⟩,
src      └───────────────────────┘
typ      └───────────────────────┘
doc      └───────────────────────┘
txt      └───────────────────────┘
par      └───────────────────────┘
pid             └────────────────┘
st   ────────────────────────────┘└─
 87      simp [prod.eq_iff_fst_eq_snd_eq] {contextual := tt}
id             └───────────────────────┘                 └┘
src      └────┘└───────────────────────┘└┘ └────────────┘└┘└─
typ      └────┘└───────────────────────┘└┘ └────────────┘└┘└─
doc      └────┘                         └┘ └────────────┘  └─
txt      └────┘                         └┘ └────────────┘  └─
par      └────┘                         └┘ └────────────┘  └─
pid                                    └────────────┘  
st   ────────────────────────────────────────────────────────
 88    end,
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
 89    inj := assume x y, eq_of_add_eq_add_right }
id                      └────────────────────┘
src                       └────────────────────┘
typ                     └────────────────────┘
 90  
 91  section
 92  variables (α)
 93  lemma uniformity_eq_comap_nhds_zero : 𝓤 α = comap (λx:α×α, x.2 - x.1) (𝓝 (0:α)) :=
id                                            └───┘                  
src                                            └───┘                  
typ                                           └───┘                  
doc                                             └───┘                      
 94  begin
st   └─────
 95    rw [nhds_eq_comap_uniformity, filter.comap_comap_comp],
id         └──────────────────────┘  └─────────────────────┘
src    └──┘└──────────────────────┘└┘└─────────────────────┘
typ    └──┘└──────────────────────┘└┘└─────────────────────┘
doc    └──┘                        └┘                       
txt    └──┘                        └┘                       
par    └──┘                        └┘                       
pid      └┘                        └┘                       
st   ─────────────────────────────┘└───────────────────────┘└──
 96    refine le_antisymm (filter.map_le_iff_le_comap.1 _) _,
id            └─────────┘  └────────────────────────┘
src    └─────┘└─────────┘ └────────────────────────┘└─────┘
typ    └─────┘└─────────┘ └────────────────────────┘└─────┘
doc    └─────┘                                      └─────┘
txt    └─────┘                                      └─────┘
par    └─────┘                                      └─────┘
pid                                                └─────┘
st   ──────────────────────────────────────────────────────┘└─
 97    { assume s hs,
src      └─────────┘
typ      └─────────┘
doc      └─────────┘
txt      └─────────┘
par      └─────────┘
pid      └─────────┘
st   ───┘└─────────┘└─
 98      rcases mem_uniformity_of_uniform_continuous_invariant uniform_continuous_sub hs with ⟨t, ht, hts⟩,
id              └────────────────────────────────────────────┘ └────────────────────┘ └┘
src      └─────┘└────────────────────────────────────────────┘└────────────────────┘  └────────────────┘
typ      └─────┘└────────────────────────────────────────────┘└────────────────────┘└┘└────────────────┘
doc      └─────┘                                                                      └────────────────┘
txt      └─────┘                                                                      └────────────────┘
par      └─────┘                                                                      └────────────────┘
pid                                                                                  └────────────────┘
st   ────────────────────────────────────────────────────────────────────────────────────────────────────┘└─
 99      refine mem_map.2 (mem_sets_of_superset ht _),
id              └─────┘    └──────────────────┘ └┘
src      └─────┘└─────┘└─┘ └──────────────────┘  └─┘
typ      └─────┘└─────┘└─┘ └──────────────────┘└┘└─┘
doc      └─────┘       └─┘                       └─┘
txt      └─────┘       └─┘                       └─┘
par      └─────┘       └─┘                       └─┘
pid                   └─┘                       └─┘
st   ───────────────────────────────────────────────┘└─
100      rintros ⟨a, b⟩,
src      └────────────┘
typ      └────────────┘
doc      └────────────┘
txt      └────────────┘
par      └────────────┘
pid             └─────┘
st   ─────────────────┘└─
101      simpa [subset_def] using hts a b a },
id              └────────┘        └─┘    
src      └─────┘└────────┘└──────┘      
typ      └─────┘└────────┘└──────┘└─┘ 
doc      └─────┘          └──────┘      
txt      └─────┘          └──────┘      
par      └─────┘          └──────┘      
pid                     └────┘      
st   ──────────────────────────────────────┘└┘
102    { assume s hs,
src      └─────────┘
typ      └─────────┘
doc      └─────────┘
txt      └─────────┘
par      └─────────┘
pid      └─────────┘
st   ──────────────┘└─
103      rcases mem_uniformity_of_uniform_continuous_invariant uniform_continuous_add hs with ⟨t, ht, hts⟩,
id              └────────────────────────────────────────────┘ └────────────────────┘ └┘
src      └─────┘└────────────────────────────────────────────┘└────────────────────┘  └────────────────┘
typ      └─────┘└────────────────────────────────────────────┘└────────────────────┘└┘└────────────────┘
doc      └─────┘                                                                      └────────────────┘
txt      └─────┘                                                                      └────────────────┘
par      └─────┘                                                                      └────────────────┘
pid                                                                                  └────────────────┘
st   ────────────────────────────────────────────────────────────────────────────────────────────────────┘└─
104      refine ⟨_, ht, _⟩,
id                  └┘
src      └─────┘ └─┘  └──┘
typ      └─────┘ └─┘└┘└──┘
doc      └─────┘ └─┘  └──┘
txt      └─────┘ └─┘  └──┘
par      └─────┘ └─┘  └──┘
pid             └─┘  └──┘
st   ────────────────────┘└─
105      rintros ⟨a, b⟩, simpa [subset_def] using hts 0 (b - a) a }
id                              └────────┘        └─┘         
src      └────────────┘  └─────┘└────────┘└──────┘   └─┘   └┘ 
typ      └────────────┘  └─────┘└────────┘└──────┘└─┘└─┘  └┘
doc      └────────────┘  └─────┘          └──────┘   └─┘    └┘ 
txt      └────────────┘  └─────┘          └──────┘   └─┘    └┘ 
par      └────────────┘  └─────┘          └──────┘   └─┘    └┘ 
pid             └─────┘                 └────┘   └─┘    └┘ 
st   ─────────────────┘└─────────────────────────────────────────┘└─
106  end
st   ──┘
107  end
108  
109  lemma group_separation_rel (x y : α) : (x, y) ∈ separation_rel α ↔ x - y ∈ closure ({0} : set α) :=
id                                              └────────────┘       └─────┘       └─┘ 
src                                                └────────────┘          └─────┘       └─┘
typ                                             └────────────┘       └─────┘       └─┘ 
doc                                                  └────────────┘             └─────┘
110  have embedding (λa, a + (y - x)), from (uniform_embedding_translate (y - x)).embedding,
id        └───────┘                    └─────────────────────────┘      └───────┘
src       └───────┘                        └─────────────────────────┘        └───────┘
typ       └───────┘                    └─────────────────────────┘      └───────┘
doc       └───────┘
111  show (x, y) ∈ ⋂₀ (𝓤 α).sets ↔ x - y ∈ closure ({0} : set α),
id             └┘    └──┘       └─────┘       └─┘ 
src              └┘     └──┘         └─────┘       └─┘
typ            └┘    └──┘       └─────┘       └─┘ 
doc                └┘                     └─────┘
112  begin
st   └─────
113    rw [this.closure_eq_preimage_closure_image, uniformity_eq_comap_nhds_zero α, sInter_comap_sets],
id                                                 └───────────────────────────┘   └───────────────┘
src    └──┘                                      └┘└───────────────────────────┘ └┘└───────────────┘
typ    └──┘└────────────────────────────────────┘└┘└───────────────────────────┘└┘└───────────────┘
doc    └──┘                                      └┘                              └┘                 
txt    └──┘                                      └┘                              └┘                 
par    └──┘                                      └┘                              └┘                 
pid      └┘                                      └┘                              └┘                 
st   ───────────────────────────────────────────┘└───────────────────────────────┘└─────────────────┘└──
114    simp [mem_closure_iff_nhds, inter_singleton_nonempty]
id           └──────────────────┘  └──────────────────────┘
src    └────┘└──────────────────┘└┘└──────────────────────┘└┘
typ    └────┘└──────────────────┘└┘└──────────────────────┘└┘
doc    └────┘                    └┘                        └┘
txt    └────┘                    └┘                        └┘
par    └────┘                    └┘                        └┘
pid                            └┘                        
st   ───────────────────────────────────────────────────────┘
115  end
st   └─┘
116  
117  lemma uniform_continuous_of_tendsto_zero [uniform_space β] [add_group β] [uniform_add_group β]
id                                             └───────────┘    └───────┘    └───────────────┘ 
src                                            └───────────┘     └───────┘     └───────────────┘
typ                                            └───────────┘    └───────┘    └───────────────┘ 
doc                                            └───────────┘                   └───────────────┘
118    {f : α → β} [is_add_group_hom f] (h : tendsto f (𝓝 0) (𝓝 0)) :
id                └──────────────┘        └─────┘        
src                 └──────────────┘         └─────┘         
typ               └──────────────┘        └─────┘        
doc                 └──────────────┘         └─────┘         
119    uniform_continuous f :=
id     └────────────────┘ 
src    └────────────────┘
typ    └────────────────┘ 
120  begin
st   └─────
121    have : ((λx:β×β, x.2 - x.1) ∘ (λx:α×α, (f x.1, f x.2))) = (λx:α×α, f (x.2 - x.1)),
id                                                                
src    └─────┘   └┘  └┘ └─┘ └──┘  └┘   └┘  └──┘  └────┘  └┘   └┘   └─┘  └──┘
typ    └─────┘   └┘ └┘ └─┘ └──┘  └┘  └┘  └──┘  └────┘  └┘  └┘  └─┘  └──┘
doc    └─────┘   └┘   └┘ └─┘  └──┘   └┘   └┘   └──┘  └────┘   └┘   └┘   └─┘  └──┘
txt    └─────┘   └┘   └┘ └─┘  └──┘   └┘   └┘   └──┘  └────┘   └┘   └┘   └─┘  └──┘
par    └─────┘   └┘   └┘ └─┘  └──┘   └┘   └┘   └──┘  └────┘   └┘   └┘   └─┘  └──┘
pid    └───┘└┘   └┘   └┘ └─┘  └──┘   └┘   └┘   └──┘  └────┘   └┘   └┘   └─┘  └──┘
st   ──────────────────────────────────────────────────────────────────────────────────┘└─
122    { simp only [is_add_group_hom.map_sub f] },
id                  └──────────────────────┘ 
src      └─────────┘└──────────────────────┘ └┘
typ      └─────────┘└──────────────────────┘└┘
doc      └─────────┘└──────────────────────┘ └┘
txt      └─────────┘                         └┘
par      └─────────┘                         └┘
pid          └──┘└┘                         
st   ───┘└─────────────────────────────────────┘└┘
123    rw [uniform_continuous, uniformity_eq_comap_nhds_zero α, uniformity_eq_comap_nhds_zero β,
id         └────────────────┘  └───────────────────────────┘   └───────────────────────────┘ 
src    └──┘└────────────────┘└┘└───────────────────────────┘ └┘└───────────────────────────┘ └─
typ    └──┘└────────────────┘└┘└───────────────────────────┘└┘└───────────────────────────┘└─
doc    └──┘                  └┘                              └┘                              └─
txt    └──┘                  └┘                              └┘                              └─
par    └──┘                  └┘                              └┘                              └─
pid      └┘                  └┘                              └┘                              └─
st   ───────────────────────┘└───────────────────────────────┘└───────────────────────────────┘└─
124      tendsto_comap_iff, this],
id       └───────────────┘  └──┘
src  ───┘└───────────────┘└┘    
typ  ───┘└───────────────┘└┘└──┘
doc  ───┘                 └┘    
txt  ───┘                 └┘    
par  ───┘                 └┘    
pid  ───┘                 └┘    
st   ────────────────────┘└────┘└──
125    exact tendsto.comp h tendsto_comap
id           └──────────┘  └───────────┘
src    └────┘└──────────┘ └───────────┘
typ    └────┘└──────────┘└───────────┘
doc    └────┘                          
txt    └────┘                          
par    └────┘                          
pid                                   
st   ────────────────────────────────────┘
126  end
st   └─┘
127  
128  lemma uniform_continuous_of_continuous [uniform_space β] [add_group β] [uniform_add_group β]
id                                           └───────────┘    └───────┘    └───────────────┘ 
src                                          └───────────┘     └───────┘     └───────────────┘
typ                                          └───────────┘    └───────┘    └───────────────┘ 
doc                                          └───────────┘                   └───────────────┘
129    {f : α → β} [is_add_group_hom f] (h : continuous f) :
id                └──────────────┘        └────────┘ 
src                 └──────────────┘         └────────┘
typ               └──────────────┘        └────────┘ 
doc                 └──────────────┘         └────────┘
130    uniform_continuous f :=
id     └────────────────┘ 
src    └────────────────┘
typ    └────────────────┘ 
131  uniform_continuous_of_tendsto_zero $
id   └────────────────────────────────┘
src  └────────────────────────────────┘
typ  └────────────────────────────────┘
132    suffices tendsto f (𝓝 0) (𝓝 (f 0)), by rwa [is_add_group_hom.map_zero f] at this,
id              └─────┘                        └───────────────────────┘ 
src             └─────┘                     └───┘└───────────────────────┘ └───────┘
typ             └─────┘                   └───┘└───────────────────────┘└───────┘
doc             └─────┘                     └───┘                          └───────┘
txt                                           └───┘                          └───────┘
par                                           └───┘                          └───────┘
pid                                              └┘                          └──────┘
st                                           └───────────────────────────────┘└──────┘
133    h.tendsto 0
id     └──────┘
src     └──────┘
typ    └──────┘
134  
135  end uniform_add_group
136  
137  section topological_add_comm_group
138  universes u v w x
139  open filter
140  
141  variables {G : Type u} [add_comm_group G] [topological_space G] [topological_add_group G]
id                           └────────────┘     └───────────────┘     └───────────────────┘
src                          └────────────┘     └───────────────┘     └───────────────────┘
typ                          └────────────┘     └───────────────┘     └───────────────────┘
doc                                             └───────────────┘     └───────────────────┘
142  
143  variable (G)
144  def topological_add_group.to_uniform_space : uniform_space G :=
id                                                └───────────┘ 
src                                               └───────────┘
typ                                               └───────────┘ 
doc                                               └───────────┘
145  { uniformity          := comap (λp:G×G, p.2 - p.1) (𝓝 0),
id                            └───┘              
src                           └───┘                  
typ                           └───┘              
doc                           └───┘                      
146    refl                :=
147      by refine map_le_iff_le_comap.1 (le_trans _ (pure_le_nhds 0));
id                 └─────────────────┘    └──────┘    └──────────┘
src         └─────┘└─────────────────┘└─┘ └──────┘└─┘ └──────────┘└──┘
typ         └─────┘└─────────────────┘└─┘ └──────┘└─┘ └──────────┘└──┘
doc         └─────┘                   └─┘         └─┘             └──┘
txt         └─────┘                   └─┘         └─┘             └──┘
par         └─────┘                   └─┘         └─┘             └──┘
pid                                  └─┘         └─┘             └──┘
st         └────────────────────────────────────────────────────────────
148        simp [set.subset_def] {contextual := tt},
id               └────────────┘                 └┘
src        └────┘└────────────┘└┘ └────────────┘└┘
typ        └────┘└────────────┘└┘ └────────────┘└┘
doc        └────┘              └┘ └────────────┘  
txt        └────┘              └┘ └────────────┘  
par        └────┘              └┘ └────────────┘  
pid                           └────────────┘  
st   ─────────────────────────────────────────────┘
149    symm                :=
150    begin
st     └─────
151      suffices : tendsto ((λp, -p) ∘ (λp:G×G, p.2 - p.1)) (comap (λp:G×G, p.2 - p.1) (𝓝 0)) (𝓝 (-0)),
id                  └─────┘                               └───┘                     
src      └─────────┘└─────┘   └─┘ └┘  └┘  └┘ └─┘ └───┘ └───┘  └┘   └┘ └─┘  └──┘ └───┘    └─┘
typ      └─────────┘└─────┘   └─┘ └┘  └┘  └┘ └─┘ └───┘ └───┘  └┘  └┘ └─┘  └──┘ └───┘    └─┘
doc      └─────────┘└─────┘   └─┘  └┘   └┘   └┘ └─┘  └───┘ └───┘  └┘   └┘ └─┘  └──┘ └───┘    └─┘
txt      └─────────┘          └─┘  └┘   └┘   └┘ └─┘  └───┘        └┘   └┘ └─┘  └──┘  └───┘    └─┘
par      └─────────┘          └─┘  └┘   └┘   └┘ └─┘  └───┘        └┘   └┘ └─┘  └──┘  └───┘    └─┘
pid      └───────┘└┘          └─┘  └┘   └┘   └┘ └─┘  └───┘        └┘   └┘ └─┘  └──┘  └───┘    └─┘
st   ─────────────────────────────────────────────────────────────────────────────────────────────────┘└─
152      { simpa [(∘), tendsto_comap_iff] },
id                    └───────────────┘
src        └─────┘└──┘└───────────────┘└┘
typ        └─────┘└──┘└───────────────┘└┘
doc        └─────┘ └──┘                 └┘
txt        └─────┘ └──┘                 └┘
par        └─────┘ └──┘                 └┘
pid              └──┘                 
st   ─────┘└─────────────────────────────┘└┘
153      exact tendsto.comp (tendsto.neg tendsto_id) tendsto_comap
id             └──────────┘  └─────────┘ └────────┘  └───────────┘
src      └────┘└──────────┘ └─────────┘└────────┘└┘└───────────┘
typ      └────┘└──────────┘ └─────────┘└────────┘└┘└───────────┘
doc      └────┘                                  └┘             
txt      └────┘                                  └┘             
par      └────┘                                  └┘             
pid                                             └┘             
st   ──────────────────────────────────────────────────────────────
154    end,
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
155    comp                :=
156    begin
st     └─────
157      intros D H,
src      └────────┘
typ      └────────┘
doc      └────────┘
txt      └────────┘
par      └────────┘
pid            └──┘
st   ─────────────┘└─
158      rw mem_lift'_sets,
id          └────────────┘
src      └─┘└────────────┘
typ      └─┘└────────────┘
doc      └─┘
txt      └─┘
par      └─┘
pid        
st   ────────────────────┘└─
159      { rcases H with ⟨U, U_nhds, U_sub⟩,
id                
src        └─────┘ └──────────────────────┘
typ        └─────┘└──────────────────────┘
doc        └─────┘ └──────────────────────┘
txt        └─────┘ └──────────────────────┘
par        └─────┘ └──────────────────────┘
pid               └──────────────────────┘
st   ─────┘└──────────────────────────────┘└─
160        rcases exists_nhds_half U_nhds with ⟨V, ⟨V_nhds, V_sum⟩⟩,
id                └──────────────┘ └────┘
src        └─────┘└──────────────┘      └────────────────────────┘
typ        └─────┘└──────────────┘└────┘└────────────────────────┘
doc        └─────┘                      └────────────────────────┘
txt        └─────┘                      └────────────────────────┘
par        └─────┘                      └────────────────────────┘
pid                                    └────────────────────────┘
st   ─────────────────────────────────────────────────────────────┘└─
161        existsi ((λp:G×G, p.2 - p.1) ⁻¹' V),
id                                     └─┘ 
src        └──────┘   └┘   └┘ └─┘  └──┘└─┘ 
typ        └──────┘   └┘  └┘ └─┘  └──┘└─┘
doc        └──────┘   └┘   └┘ └─┘  └──┘└─┘ 
txt        └──────┘   └┘   └┘ └─┘  └──┘    
par        └──────┘   └┘   └┘ └─┘  └──┘    
pid                  └┘   └┘ └─┘  └──┘    
st   ────────────────────────────────────────┘└─
162        have H : (λp:G×G, p.2 - p.1) ⁻¹' V ∈ comap (λp:G×G, p.2 - p.1) (𝓝 (0 : G)),
id                                            └───┘                             
src        └───────┘  └┘   └┘ └─┘  └──┘    └───┘  └┘   └┘ └─┘  └──┘   └──┘ └┘
typ        └───────┘  └┘   └┘ └─┘  └──┘   └───┘  └┘   └┘ └─┘  └──┘   └──┘└┘
doc        └───────┘  └┘   └┘ └─┘  └──┘     └───┘  └┘   └┘ └─┘  └──┘   └──┘ └┘
txt        └───────┘  └┘   └┘ └─┘  └──┘            └┘   └┘ └─┘  └──┘   └──┘ └┘
par        └───────┘  └┘   └┘ └─┘  └──┘            └┘   └┘ └─┘  └──┘   └──┘ └┘
pid        └────┘└─┘  └┘   └┘ └─┘  └──┘            └┘   └┘ └─┘  └──┘   └──┘ └┘
st   ───────────────────────────────────────────────────────────────────────────────┘
163          by existsi [V, V_nhds] ; refl,
id                         └────┘
src             └───────┘ └┘      └┘  └──┘
typ             └───────┘└┘└────┘└┘  └──┘
doc             └───────┘ └┘      └┘  └──┘
txt             └───────┘ └┘      └┘  └──┘
par             └───────┘ └┘      └┘  └──┘
pid                    └┘ └┘      
st                                        └─
164        existsi H,
id                 
src        └──────┘
typ        └──────┘
doc        └──────┘
txt        └──────┘
par        └──────┘
pid               
st   ──────────────┘└─
165        have comp_rel_sub : comp_rel ((λp:G×G, p.2 - p.1) ⁻¹' V) ((λp:G×G, p.2 - p.1) ⁻¹' V) ⊆ (λp:G×G, p.2 - p.1) ⁻¹' U,
id                             └──────┘                                                                                
src        └──────────────────┘└──────┘   └┘   └┘ └─┘  └──┘    └┘   └┘   └┘ └─┘  └──┘    └┘  └┘   └┘ └─┘  └──┘   
typ        └──────────────────┘└──────┘   └┘   └┘ └─┘  └──┘    └┘   └┘   └┘ └─┘  └──┘   └┘  └┘  └┘ └─┘  └──┘   
doc        └──────────────────┘└──────┘   └┘   └┘ └─┘  └──┘    └┘   └┘   └┘ └─┘  └──┘    └┘   └┘   └┘ └─┘  └──┘   
txt        └──────────────────┘           └┘   └┘ └─┘  └──┘    └┘   └┘   └┘ └─┘  └──┘    └┘   └┘   └┘ └─┘  └──┘   
par        └──────────────────┘           └┘   └┘ └─┘  └──┘    └┘   └┘   └┘ └─┘  └──┘    └┘   └┘   └┘ └─┘  └──┘   
pid        └───────────────┘└─┘           └┘   └┘ └─┘  └──┘    └┘   └┘   └┘ └─┘  └──┘    └┘   └┘   └┘ └─┘  └──┘   
st   ─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘└─
166        begin
st   ──────────┘
167          intros p p_comp_rel,
src          └─────────────────┘
typ          └─────────────────┘
doc          └─────────────────┘
txt          └─────────────────┘
par          └─────────────────┘
pid                └───────────┘
st   ──────────────────────────┘└─
168          rcases p_comp_rel with ⟨z, ⟨Hz1, Hz2⟩⟩,
id                  └────────┘
src          └─────┘          └───────────────────┘
typ          └─────┘└────────┘└───────────────────┘
doc          └─────┘          └───────────────────┘
txt          └─────┘          └───────────────────┘
par          └─────┘          └───────────────────┘
pid                          └───────────────────┘
st   ─────────────────────────────────────────────┘└─
169          simpa using V_sum _ _ Hz1 Hz2
id                       └───┘     └─┘ └─┘
src          └──────────┘     └───┘      
typ          └──────────┘└───┘└───┘└─┘└─┘
doc          └──────────┘     └───┘      
txt          └──────────┘     └───┘      
par          └──────────┘     └───┘      
pid               └────┘     └───┘      
st   ──────────────────────────────────────
170        end,
src  ─────┘
typ  ─────┘
doc  ─────┘
txt  ─────┘
par  ─────┘
pid  ─────┘
st   ─────┘└─┘└─
171        exact set.subset.trans comp_rel_sub U_sub },
id               └──────────────┘ └──────────┘ └───┘
src        └────┘└──────────────┘                 
typ        └────┘└──────────────┘└──────────┘└───┘
doc        └────┘                                 
txt        └────┘                                 
par        └────┘                                 
pid                                              
st   ───────────────────────────────────────────────┘└┘
172      { exact monotone_comp_rel monotone_id monotone_id }
id               └───────────────┘             └─────────┘
src        └────┘└───────────────┘           └─────────┘
typ        └────┘└───────────────┘           └─────────┘
doc        └────┘                                       
txt        └────┘                                       
par        └────┘                                       
pid                                                    
st   ─────────────────────────────────────────────────────┘└─
173    end,
st   ────┘
174    is_open_uniformity  :=
175    begin
st     └─────
176      intro S,
src      └─────┘
typ      └─────┘
doc      └─────┘
txt      └─────┘
par      └─────┘
pid           └┘
st   ──────────┘└─
177      let S' := λ x, {p : G × G | p.1 = x → p.2 ∈ S},
id                                                
src      └────────┘ └──┘└──┘   └─┘ └─┘   └─┘  
typ      └────────┘ └──┘└──┘  └─┘ └─┘   └─┘ 
doc      └────────┘ └──┘ └──┘   └─┘ └─┘    └─┘  
txt      └────────┘ └──┘ └──┘   └─┘ └─┘    └─┘  
par      └────────┘ └──┘ └──┘   └─┘ └─┘    └─┘  
pid      └────┘└─┘ └──┘ └──┘   └─┘ └─┘    └─┘  
st   ─────────────────────────────────────────────────┘└─
178      show is_open S ↔ ∀ (x : G), x ∈ S → S' x ∈ comap (λp:G×G, p.2 - p.1) (𝓝 (0 : G)),
id            └─────┘                      └┘     └───┘                             
src      └───┘└─────┘   └────┘          └───┘  └┘   └┘ └─┘  └──┘   └──┘ └┘
typ      └───┘└─────┘   └────┘    └┘  └───┘  └┘   └┘ └─┘  └──┘   └──┘└┘
doc      └───┘└─────┘   └────┘          └───┘  └┘   └┘ └─┘  └──┘   └──┘ └┘
txt      └───┘          └────┘                 └┘   └┘ └─┘  └──┘   └──┘ └┘
par      └───┘          └────┘                 └┘   └┘ └─┘  └──┘   └──┘ └┘
pid      └───┘          └────┘                 └┘   └┘ └─┘  └──┘   └──┘ └┘
st   ───────────────────────────────────────────────────────────────────────────────────┘└─
179      rw [is_open_iff_mem_nhds],
id           └──────────────────┘
src      └──┘└──────────────────┘
typ      └──┘└──────────────────┘
doc      └──┘                    
txt      └──┘                    
par      └──┘                    
pid        └┘                    
st   ───────────────────────────┘└──
180      refine forall_congr (assume a, forall_congr (assume ha, _)),
id                                      └──────────┘
src      └─────┘                   └──┘└──────────┘       └──────┘
typ      └─────┘                   └──┘└──────────┘       └──────┘
doc      └─────┘                   └──┘                   └──────┘
txt      └─────┘                   └──┘                   └──────┘
par      └─────┘                   └──┘                   └──────┘
pid                               └──┘                   └──────┘
st   ──────────────────────────────────────────────────────────────┘└─
181      rw [← nhds_translation a, mem_comap_sets, mem_comap_sets],
id             └──────────────┘   └────────────┘  └────────────┘
src      └────┘└──────────────┘ └┘└────────────┘└┘└────────────┘
typ      └────┘└──────────────┘└┘└────────────┘└┘└────────────┘
doc      └────┘                 └┘              └┘              
txt      └────┘                 └┘              └┘              
par      └────┘                 └┘              └┘              
pid        └──┘                 └┘              └┘              
st   ───────────────────────────┘└──────────────┘└──────────────┘└──
182      refine exists_congr (assume t, exists_congr (assume ht, _)),
id                                      └──────────┘
src      └─────┘                   └──┘└──────────┘       └──────┘
typ      └─────┘                   └──┘└──────────┘       └──────┘
doc      └─────┘                   └──┘                   └──────┘
txt      └─────┘                   └──┘                   └──────┘
par      └─────┘                   └──┘                   └──────┘
pid                               └──┘                   └──────┘
st   ──────────────────────────────────────────────────────────────┘└─
183      show (λ (y : G), y - a) ⁻¹' t ⊆ S ↔ (λ (p : G × G), p.snd - p.fst) ⁻¹' t ⊆ S' a,
id                                                          └──┘    └──┘         └┘ 
src      └───┘  └────┘ └─┘   └┘         └────┘   └─┘ └──┘  └──┘└┘       
typ      └───┘  └────┘ └─┘   └┘        └────┘  └─┘ └──┘  └──┘└┘    └┘
doc      └───┘  └────┘ └─┘   └┘         └────┘   └─┘           └┘       
txt      └───┘  └────┘ └─┘   └┘         └────┘   └─┘           └┘       
par      └───┘  └────┘ └─┘   └┘         └────┘   └─┘           └┘       
pid      └───┘  └────┘ └─┘   └┘         └────┘   └─┘           └┘       
st   ─────────────────────────────────────────────────────────────────────────────────────
184      split,
src      └───┘
typ      └───┘
doc      └───┘
txt      └───┘
par      └───┘
st   ────────┘└─
185      { rintros h ⟨x, y⟩ hx rfl, exact h hx },
id                                         └┘
src        └─────────────────────┘  └────┘   
typ        └─────────────────────┘  └────┘└┘
doc        └─────────────────────┘  └────┘   
txt        └─────────────────────┘  └────┘   
par        └─────────────────────┘  └────┘   
pid               └──────────────┘          
st   ─────┘└─────────────────────┘└───────────┘└┘
186      { rintros h x hx, exact @h (a, x) hx rfl }
id                                      └┘ └─┘
src        └────────────┘  └────┘    └┘ └┘  └─┘
typ        └────────────┘  └────┘  └┘└┘└┘└─┘
doc        └────────────┘  └────┘    └┘ └┘     
txt        └────────────┘  └────┘    └┘ └┘     
par        └────────────┘  └────┘    └┘ └┘     
pid               └─────┘           └┘ └┘     
st   ───────────────────┘└───────────────────────┘└─
187    end }
st   ────┘
188  
189  section
190  local attribute [instance] topological_add_group.to_uniform_space
id                              └────────────────────────────────────┘
src                             └────────────────────────────────────┘
typ                             └────────────────────────────────────┘
191  
192  lemma uniformity_eq_comap_nhds_zero' : 𝓤 G = comap (λp:G×G, p.2 - p.1) (𝓝 (0 : G)) := rfl
id                                             └───┘                          └─┘
src                                             └───┘                               └─┘
typ                                            └───┘                          └─┘
doc                                              └───┘                      
193  
194  variable {G}
195  lemma topological_add_group_is_uniform : uniform_add_group G :=
id                                            └───────────────┘ 
src                                           └───────────────┘
typ                                           └───────────────┘ 
doc                                           └───────────────┘
196  have tendsto
id        └─────┘
src       └─────┘
typ       └─────┘
doc       └─────┘
197      ((λp:(G×G), p.1 - p.2) ∘ (λp:(G×G)×(G×G), (p.1.2 - p.1.1, p.2.2 - p.2.1)))
id                                              
src                                                         
typ                                             
198      (comap (λp:(G×G)×(G×G), (p.1.2 - p.1.1, p.2.2 - p.2.1)) ((𝓝 0).prod (𝓝 0)))
id        └───┘                                 └──┘   
src       └───┘                                         └──┘   
typ       └───┘                                 └──┘   
doc       └───┘                                                       └──┘   
199      (𝓝 (0 - 0)) :=
id            
src           
typ           
doc       
200    (tendsto_fst.sub tendsto_snd).comp tendsto_comap,
id      └─────────┘└──┘ └─────────┘ └──┘  └───────────┘
src     └─────────┘└──┘ └─────────┘ └──┘  └───────────┘
typ     └─────────┘└──┘ └─────────┘ └──┘  └───────────┘
201  begin
st   └─────
202    constructor,
src    └─────────┘
typ    └─────────┘
doc    └─────────┘
txt    └─────────┘
par    └─────────┘
st   ────────────┘└─
203    rw [uniform_continuous, uniformity_prod_eq_prod, tendsto_map'_iff,
id         └────────────────┘  └─────────────────────┘  └──────────────┘
src    └──┘└────────────────┘└┘└─────────────────────┘└┘└──────────────┘└─
typ    └──┘└────────────────┘└┘└─────────────────────┘└┘└──────────────┘└─
doc    └──┘                  └┘                       └┘                └─
txt    └──┘                  └┘                       └┘                └─
par    └──┘                  └┘                       └┘                └─
pid      └┘                  └┘                       └┘                └─
st   ───────────────────────┘└───────────────────────┘└────────────────┘└─
204      uniformity_eq_comap_nhds_zero' G, tendsto_comap_iff, prod_comap_comap_eq],
id                                        └───────────────┘  └─────────────────┘
src  ───┘                               └┘└───────────────┘└┘└─────────────────┘
typ  ───┘                              └┘└───────────────┘└┘└─────────────────┘
doc  ───┘                               └┘                 └┘                   
txt  ───┘                               └┘                 └┘                   
par  ───┘                               └┘                 └┘                   
pid  ───┘                               └┘                 └┘                   
st   ───────────────────────────────────┘└─────────────────┘└───────────────────┘└──
205    simpa [(∘)]
id            
src    └─────┘└──┘
typ    └─────┘└──┘
doc    └─────┘ └──┘
txt    └─────┘ └──┘
par    └─────┘ └──┘
pid          └─┘
st   ─────────────┘
206  end
st   └─┘
207  end
208  
209  lemma to_uniform_space_eq {α : Type*} [u : uniform_space α] [add_comm_group α] [uniform_add_group α]:
id                                              └───────────┘    └────────────┘    └───────────────┘ 
src                                             └───────────┘     └────────────┘     └───────────────┘
typ                                             └───────────┘    └────────────┘    └───────────────┘ 
doc                                             └───────────┘                        └───────────────┘
210    topological_add_group.to_uniform_space α = u :=
id     └────────────────────────────────────┘   
src    └────────────────────────────────────┘   
typ    └────────────────────────────────────┘   
211  begin
st   └─────
212    ext : 1,
src    └─────┘
typ    └─────┘
doc    └─────┘
txt    └─────┘
par    └─────┘
pid       └┘
st   ────────┘└─
213    show @uniformity α (topological_add_group.to_uniform_space α) = 𝓤 α,
id           └────────┘                                                 
src    └───┘ └────────┘                                         └┘ 
typ    └───┘ └────────┘                                         └┘ 
doc    └───┘ └────────┘                                         └┘  
txt    └───┘                                                    └┘  
par    └───┘                                                    └┘  
pid    └───┘                                                    └┘  
st   ────────────────────────────────────────────────────────────────────┘└─
214    rw [uniformity_eq_comap_nhds_zero' α, uniformity_eq_comap_nhds_zero α]
id                                          └───────────────────────────┘ 
src    └──┘                               └┘└───────────────────────────┘ └┘
typ    └──┘                              └┘└───────────────────────────┘└┘
doc    └──┘                               └┘                              └┘
txt    └──┘                               └┘                              └┘
par    └──┘                               └┘                              └┘
pid      └┘                               └┘                              
st   ─────────────────────────────────────┘└───────────────────────────────┘
215  end
st   └─┘
216  
217  end topological_add_comm_group
218  
219  namespace add_comm_group
220  section Z_bilin
221  
222  variables {α : Type*} {β : Type*} {γ : Type*} {δ : Type*}
id                  └───┘       └───┘       └───┘
typ                 └───┘       └───┘       └───┘
223  variables [add_comm_group α] [add_comm_group β] [add_comm_group γ]
id              └────────────┘     └────────────┘     └────────────┘
src             └────────────┘     └────────────┘     └────────────┘
typ             └────────────┘     └────────────┘     └────────────┘
224  
225  /- TODO: when modules are changed to have more explicit base ring, then change replace `is_Z_bilin`
226  by using `is_bilinear_map ℤ` from `tensor_product`. -/
227  class is_Z_bilin (f : α × β → γ) : Prop :=
id                             
src                          
typ                            
228  (add_left  : ∀ a a' b, f (a + a', b) = f (a, b) + f (a', b))
id                   └┘      └┘            └┘  
src                                                 
typ                  └┘      └┘            └┘  
229  (add_right : ∀ a b b', f (a, b + b') = f (a, b) + f (a, b'))
id                    └┘       └┘            └┘
src                                                 
typ                   └┘       └┘            └┘
230  
231  variables (f : α × β → γ) [is_Z_bilin f]
id                             └────────┘
src                            └────────┘
typ                            └────────┘
232  
233  instance is_Z_bilin.comp_hom {g : γ → δ} [add_comm_group δ] [is_add_group_hom g] :
id                                           └────────────┘    └──────────────┘ 
src                                            └────────────┘     └──────────────┘
typ                                          └────────────┘    └──────────────┘ 
doc                                                               └──────────────┘
234    is_Z_bilin (g ∘ f) :=
id     └────────┘    
src    └────────┘    
typ    └────────┘    
235  by constructor; simp [(∘), is_Z_bilin.add_left f, is_Z_bilin.add_right f, is_add_hom.map_add g]
id                             └─────────────────┘   └──────────────────┘   └────────────────┘ 
src     └─────────┘  └────┘└──┘└─────────────────┘ └┘└──────────────────┘ └┘└────────────────┘ └─
typ     └─────────┘  └────┘└──┘└─────────────────┘└┘└──────────────────┘└┘└────────────────┘└─
doc     └─────────┘  └────┘ └──┘                    └┘                     └┘                   └─
txt     └─────────┘  └────┘ └──┘                    └┘                     └┘                   └─
par     └─────────┘  └────┘ └──┘                    └┘                     └┘                   └─
pid                       └──┘                    └┘                     └┘                   
st     └─────────────────────────────────────────────────────────────────────────────────────────────
236  
src  
typ  
doc  
txt  
par  
pid  
st   
237  instance is_Z_bilin.comp_swap : is_Z_bilin (f ∘ prod.swap) :=
id                                   └────────┘    └───────┘
src                                  └────────┘     └───────┘
typ                                  └────────┘    └───────┘
doc                                                  └───────┘
238  ⟨λ a a' b, is_Z_bilin.add_right f b a a',
id       └┘   └──────────────────┘    └┘
src             └──────────────────┘
typ      └┘   └──────────────────┘    └┘
239   λ a b b', is_Z_bilin.add_left f b b' a⟩
id        └┘  └─────────────────┘   └┘ 
src             └─────────────────┘
typ       └┘  └─────────────────┘   └┘ 
240  
241  lemma is_Z_bilin.zero_left : ∀ b, f (0, b) = 0 :=
id                                          
src                                            
typ                                         
242  begin
st   └─────
243    intro b,
src    └─────┘
typ    └─────┘
doc    └─────┘
txt    └─────┘
par    └─────┘
pid         └┘
st   ────────┘└─
244    apply add_self_iff_eq_zero.1,
id           └──────────────────┘
src    └────┘└──────────────────┘└┘
typ    └────┘└──────────────────┘└┘
doc    └────┘                    └┘
txt    └────┘                    └┘
par    └────┘                    └┘
pid                             └┘
st   ─────────────────────────────┘└─
245    rw ←is_Z_bilin.add_left f,
id         └─────────────────┘ 
src    └──┘└─────────────────┘
typ    └──┘└─────────────────┘
doc    └──┘                   
txt    └──┘                   
par    └──┘                   
pid      └┘                   
st   ──────────────────────────┘└─
246    simp
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
pid        
st   ──────┘
247  end
st   └─┘
248  
249  lemma is_Z_bilin.zero_right : ∀ a, f (a, 0) = 0 :=
id                                           
src                                             
typ                                          
250  is_Z_bilin.zero_left (f ∘ prod.swap)
id   └──────────────────┘    └───────┘
src  └──────────────────┘     └───────┘
typ  └──────────────────┘    └───────┘
doc                            └───────┘
251  
252  lemma is_Z_bilin.zero : f (0, 0) = 0 :=
id                                  
src                                  
typ                                 
253  is_Z_bilin.zero_left f 0
id   └──────────────────┘ 
src  └──────────────────┘
typ  └──────────────────┘ 
254  
255  lemma is_Z_bilin.neg_left  : ∀ a b, f (-a, b) = -f (a, b) :=
id                                              
src                                                 
typ                                             
256  begin
st   └─────
257    intros a b,
src    └────────┘
typ    └────────┘
doc    └────────┘
txt    └────────┘
par    └────────┘
pid          └──┘
st   ───────────┘└─
258    apply eq_of_sub_eq_zero,
id           └───────────────┘
src    └────┘└───────────────┘
typ    └────┘└───────────────┘
doc    └────┘
txt    └────┘
par    └────┘
pid         
st   ────────────────────────┘└─
259    rw [sub_eq_add_neg, neg_neg, ←is_Z_bilin.add_left f, neg_add_self, is_Z_bilin.zero_left f]
id         └────────────┘  └─────┘   └─────────────────┘   └──────────┘  └──────────────────┘ 
src    └──┘└────────────┘└┘└─────┘└─┘└─────────────────┘ └┘└──────────┘└┘└──────────────────┘ └┘
typ    └──┘└────────────┘└┘└─────┘└─┘└─────────────────┘└┘└──────────┘└┘└──────────────────┘└┘
doc    └──┘              └┘       └─┘                    └┘            └┘                     └┘
txt    └──┘              └┘       └─┘                    └┘            └┘                     └┘
par    └──┘              └┘       └─┘                    └┘            └┘                     └┘
pid      └┘              └┘       └─┘                    └┘            └┘                     
st   ───────────────────┘└───────┘└──────────────────────┘└────────────┘└──────────────────────┘
260  end
st   └─┘
261  
262  lemma is_Z_bilin.neg_right  : ∀ a b, f (a, -b) = -f (a, b) :=
id                                               
src                                                  
typ                                              
263  assume a b, is_Z_bilin.neg_left (f ∘ prod.swap) b a
id             └─────────────────┘    └───────┘   
src              └─────────────────┘     └───────┘
typ            └─────────────────┘    └───────┘   
doc                                       └───────┘
264  
265  lemma is_Z_bilin.sub_left : ∀ a a' b, f (a - a', b) = f (a, b) - f (a', b) :=
id                                  └┘      └┘            └┘  
src                                                                
typ                                 └┘      └┘            └┘  
266  begin
st   └─────
267    intros,
src    └────┘
typ    └────┘
doc    └────┘
txt    └────┘
par    └────┘
st   ───────┘└─
268    dsimp [algebra.sub],
id            └─────────┘
src    └─────┘└─────────┘
typ    └─────┘└─────────┘
doc    └─────┘           
txt    └─────┘           
par    └─────┘           
pid                    
st   ────────────────────┘└─
269    rw [is_Z_bilin.add_left f, is_Z_bilin.neg_left f]
id         └─────────────────┘   └─────────────────┘ 
src    └──┘└─────────────────┘ └┘└─────────────────┘ └┘
typ    └──┘└─────────────────┘└┘└─────────────────┘└┘
doc    └──┘                    └┘                    └┘
txt    └──┘                    └┘                    └┘
par    └──┘                    └┘                    └┘
pid      └┘                    └┘                    
st   ──────────────────────────┘└─────────────────────┘
270  end
st   └─┘
271  
272  lemma is_Z_bilin.sub_right : ∀ a b b', f (a, b - b') = f (a, b) - f (a,b') :=
id                                    └┘       └┘           └┘
src                                                                 
typ                                   └┘       └┘           └┘
273  assume a b b', is_Z_bilin.sub_left (f ∘ prod.swap) b b' a
id            └┘  └─────────────────┘    └───────┘   └┘ 
src                 └─────────────────┘     └───────┘
typ           └┘  └─────────────────┘    └───────┘   └┘ 
doc                                          └───────┘
274  end Z_bilin
275  end add_comm_group
276  
277  open add_comm_group filter set function
278  
279  section
280  variables {α : Type*} {β : Type*} {γ : Type*} {δ : Type*}
281  
282  -- α, β and G are abelian topological groups, G is a uniform space
283  variables [topological_space α] [add_comm_group α]
id              └───────────────┘     └────────────┘
src             └───────────────┘     └────────────┘
typ             └───────────────┘     └────────────┘
doc             └───────────────┘
284  variables [topological_space β] [add_comm_group β]
id              └───────────────┘     └────────────┘
src             └───────────────┘     └────────────┘
typ             └───────────────┘     └────────────┘
doc             └───────────────┘
285  variables {G : Type*} [uniform_space G] [add_comm_group G]
id                          └───────────┘     └────────────┘
src                         └───────────┘     └────────────┘
typ                         └───────────┘     └────────────┘
doc                         └───────────┘
286  
287  variables {ψ : α × β → G} (hψ : continuous ψ) [ψbilin : is_Z_bilin ψ]
id                                  └────────┘              └────────┘
src                                 └────────┘              └────────┘
typ                                 └────────┘              └────────┘
doc                                  └────────┘
288  
289  include hψ ψbilin
290  
291  lemma is_Z_bilin.tendsto_zero_left (x₁ : α) : tendsto ψ (𝓝 (x₁, 0)) (𝓝 0) :=
id                                                └─────┘    └┘       
src                                                └─────┘              
typ                                               └─────┘    └┘       
doc                                                └─────┘               
292  begin
st   └─────
293    have := hψ.tendsto (x₁, 0),
id             └────────┘ └┘
src    └──────┘└────────┘  └──┘
typ    └──────┘└────────┘└┘└──┘
doc    └──────┘             └──┘
txt    └──────┘             └──┘
par    └──────┘             └──┘
pid    └───┘└─┘             └──┘
st   ───────────────────────────┘└─
294    rwa [is_Z_bilin.zero_right ψ] at this
id          └───────────────────┘ 
src    └───┘└───────────────────┘ └────────┘
typ    └───┘└───────────────────┘└────────┘
doc    └───┘                      └────────┘
txt    └───┘                      └────────┘
par    └───┘                      └────────┘
pid       └┘                      └──────┘
st   ─────────────────────────────┘└───────┘
295  end
st   └─┘
296  
297  lemma is_Z_bilin.tendsto_zero_right (y₁ : β) : tendsto ψ (𝓝 (0, y₁)) (𝓝 0) :=
id                                                 └─────┘       └┘    
src                                                 └─────┘              
typ                                                └─────┘       └┘    
doc                                                 └─────┘               
298  begin
st   └─────
299    have := hψ.tendsto (0, y₁),
id             └────────┘    └┘
src    └──────┘└────────┘└─┘  
typ    └──────┘└────────┘└─┘└┘
doc    └──────┘           └─┘  
txt    └──────┘           └─┘  
par    └──────┘           └─┘  
pid    └───┘└─┘           └─┘  
st   ───────────────────────────┘└─
300    rwa [is_Z_bilin.zero_left ψ] at this
id          └──────────────────┘ 
src    └───┘└──────────────────┘ └────────┘
typ    └───┘└──────────────────┘└────────┘
doc    └───┘                     └────────┘
txt    └───┘                     └────────┘
par    └───┘                     └────────┘
pid       └┘                     └──────┘
st   ────────────────────────────┘└───────┘
301  end
st   └─┘
302  end
303  
304  section
305  variables {α : Type*} {β : Type*}
306  variables [topological_space α] [add_comm_group α] [topological_add_group α]
id              └───────────────┘    └────────────┘     └───────────────────┘
src             └───────────────┘     └────────────┘     └───────────────────┘
typ             └───────────────┘    └────────────┘     └───────────────────┘
doc             └───────────────┘                        └───────────────────┘
307  
308  -- β is a dense subgroup of α, inclusion is denoted by e
309  variables [topological_space β] [add_comm_group β]
id              └───────────────┘     └────────────┘
src             └───────────────┘     └────────────┘
typ             └───────────────┘     └────────────┘
doc             └───────────────┘
310  variables {e : β → α} [is_add_group_hom e] (de : dense_inducing e)
id                          └──────────────┘          └────────────┘
src                         └──────────────┘          └────────────┘
typ                         └──────────────┘          └────────────┘
doc                         └──────────────┘          └────────────┘
311  include de
312  
313  lemma tendsto_sub_comap_self (x₀ : α) :
id                                      
typ                                     
314    tendsto (λt:β×β, t.2 - t.1) (comap (λp:β×β, (e p.1, e p.2)) $ 𝓝 (x₀, x₀)) (𝓝 0) :=
id     └─────┘              └───┘                   └┘  └┘    
src    └─────┘                  └───┘                                   
typ    └─────┘              └───┘                   └┘  └┘    
doc    └─────┘                      └───┘                                        
315  begin
st   └─────
316    have comm : (λx:α×α, x.2-x.1) ∘ (λt:β×β, (e t.1, e t.2)) = e ∘ (λt:β×β, t.2 - t.1),
id                                                                  
src    └──────────┘  └┘  └┘ └┘ └──┘  └┘   └┘  └──┘  └───┘    └┘   └┘ └─┘  └─┘
typ    └──────────┘  └┘ └┘ └┘ └──┘  └┘  └┘  └──┘  └───┘   └┘  └┘ └─┘  └─┘
doc    └──────────┘  └┘   └┘ └┘  └──┘   └┘   └┘   └──┘  └───┘     └┘   └┘ └─┘  └─┘
txt    └──────────┘  └┘   └┘ └┘  └──┘   └┘   └┘   └──┘  └───┘     └┘   └┘ └─┘  └─┘
par    └──────────┘  └┘   └┘ └┘  └──┘   └┘   └┘   └──┘  └───┘     └┘   └┘ └─┘  └─┘
pid    └───────┘└─┘  └┘   └┘ └┘  └──┘   └┘   └┘   └──┘  └───┘     └┘   └┘ └─┘  └─┘
st   ───────────────────────────────────────────────────────────────────────────────────┘└─
317    { ext t,
src      └───┘
typ      └───┘
doc      └───┘
txt      └───┘
par      └───┘
pid         └┘
st   ───┘└───┘└─
318      change e t.2 - e t.1 = e (t.2 - t.1),
id                                      
src      └─────┘  └─┘   └─┘    └─┘  └─┘
typ      └─────┘  └─┘   └─┘   └─┘ └─┘
doc      └─────┘  └─┘   └─┘    └─┘  └─┘
txt      └─────┘  └─┘   └─┘    └─┘  └─┘
par      └─────┘  └─┘   └─┘    └─┘  └─┘
pid              └─┘   └─┘    └─┘  └─┘
st   ───────────────────────────────────────┘└─
319      rwa ← is_add_group_hom.map_sub e t.2 t.1 },
id             └──────────────────────┘      
src      └────┘└──────────────────────┘  └─┘ └─┘
typ      └────┘└──────────────────────┘ └─┘└─┘
doc      └────┘└──────────────────────┘  └─┘ └─┘
txt      └────┘                          └─┘ └─┘
par      └────┘                          └─┘ └─┘
pid         └─┘                          └─┘ └─┘
st   ────────────────────────────────────────────┘└┘
320    have lim : tendsto (λ x : α × α, x.2-x.1) (𝓝 (x₀, x₀)) (𝓝 (e 0)),
id                └─────┘                             └┘       
src    └─────────┘└─────┘  └───┘   └┘ └┘  └──┘   └┘  └─┘    └──┘
typ    └─────────┘└─────┘  └───┘  └┘ └┘  └──┘   └┘└┘└─┘   └──┘
doc    └─────────┘└─────┘  └───┘   └┘ └┘  └──┘    └┘  └─┘    └──┘
txt    └─────────┘         └───┘   └┘ └┘  └──┘     └┘  └─┘    └──┘
par    └─────────┘         └───┘   └┘ └┘  └──┘     └┘  └─┘    └──┘
pid    └──────┘└─┘         └───┘   └┘ └┘  └──┘     └┘  └─┘    └──┘
st   ─────────────────────────────────────────────────────────────────┘└─
321      { have := (continuous_sub.comp continuous_swap).tendsto (x₀, x₀),
id                  └─────────────────┘ └─────────────┘              └┘
src        └──────┘ └─────────────────┘└─────────────┘└────────┘  └┘  
typ        └──────┘ └─────────────────┘└─────────────┘└────────┘  └┘└┘
doc        └──────┘                                   └────────┘   └┘  
txt        └──────┘                                   └────────┘   └┘  
par        └──────┘                                   └────────┘   └┘  
pid        └───┘└─┘                                   └────────┘   └┘  
st   ─────┘└────────────────────────────────────────────────────────────┘└─
322        simpa [-sub_eq_add_neg, sub_self, eq.symm (is_add_group_hom.map_zero e)] using this },
id                                 └──────┘  └─────┘  └───────────────────────┘          └──┘
src        └──────────────────────┘└──────┘└┘└─────┘ └───────────────────────┘ └───────┘    
typ        └──────────────────────┘└──────┘└┘└─────┘ └───────────────────────┘└───────┘└──┘
doc        └──────────────────────┘        └┘                                  └───────┘    
txt        └──────────────────────┘        └┘                                  └───────┘    
par        └──────────────────────┘        └┘                                  └───────┘    
pid             └────────────────┘        └┘                                  └┘└────┘    
st   ─────────────────────────────────────────────────────────────────────────────────────────┘└┘
323    have := de.tendsto_comap_nhds_nhds lim comm,
id             └────────────────────────┘ └─┘ └──┘
src    └──────┘└────────────────────────┘└─┘
typ    └──────┘└────────────────────────┘└─┘└──┘
doc    └──────┘└────────────────────────┘└─┘
txt    └──────┘                             
par    └──────┘                             
pid    └───┘└─┘                             
st   ────────────────────────────────────────────┘└─
324    simp [-sub_eq_add_neg, this]
id                            └──┘
src    └─────────────────────┘    └┘
typ    └─────────────────────┘└──┘└┘
doc    └─────────────────────┘    └┘
txt    └─────────────────────┘    └┘
par    └─────────────────────┘    └┘
pid        └────────────────┘    
st   ──────────────────────────────┘
325  end
st   └─┘
326  end
327  
328  namespace dense_inducing
329  variables {α : Type*} {β : Type*} {γ : Type*} {δ : Type*}
330  variables {G : Type*}
331  
332  -- β is a dense subgroup of α, inclusion is denoted by e
333  -- δ is a dense subgroup of γ, inclusion is denoted by f
334  variables [topological_space α] [add_comm_group α] [topological_add_group α]
id              └───────────────┘    └────────────┘     └───────────────────┘
src             └───────────────┘     └────────────┘     └───────────────────┘
typ             └───────────────┘    └────────────┘     └───────────────────┘
doc             └───────────────┘                        └───────────────────┘
335  variables [topological_space β] [add_comm_group β] [topological_add_group β]
id              └───────────────┘     └────────────┘     └───────────────────┘
src             └───────────────┘     └────────────┘     └───────────────────┘
typ             └───────────────┘     └────────────┘     └───────────────────┘
doc             └───────────────┘                        └───────────────────┘
336  variables [topological_space γ] [add_comm_group γ] [topological_add_group γ]
id              └───────────────┘     └────────────┘     └───────────────────┘
src             └───────────────┘     └────────────┘     └───────────────────┘
typ             └───────────────┘     └────────────┘     └───────────────────┘
doc             └───────────────┘                        └───────────────────┘
337  variables [topological_space δ] [add_comm_group δ] [topological_add_group δ]
id              └───────────────┘     └────────────┘     └───────────────────┘
src             └───────────────┘     └────────────┘     └───────────────────┘
typ             └───────────────┘     └────────────┘     └───────────────────┘
doc             └───────────────┘                        └───────────────────┘
338  variables [uniform_space G] [add_comm_group G] [uniform_add_group G] [separated G] [complete_space G]
id              └───────────┘     └────────────┘     └───────────────┘     └───────┘     └────────────┘
src             └───────────┘     └────────────┘     └───────────────┘     └───────┘     └────────────┘
typ             └───────────┘     └────────────┘     └───────────────┘     └───────┘     └────────────┘
doc             └───────────┘                        └───────────────┘                   └────────────┘
339  variables {e : β → α} [is_add_group_hom e] (de : dense_inducing e)
id                          └──────────────┘          └────────────┘
src                         └──────────────┘          └────────────┘
typ                         └──────────────┘          └────────────┘
doc                         └──────────────┘          └────────────┘
340  variables {f : δ → γ} [is_add_group_hom f] (df : dense_inducing f)
id                          └──────────────┘          └────────────┘
src                         └──────────────┘          └────────────┘
typ                         └──────────────┘          └────────────┘
doc                         └──────────────┘          └────────────┘
341  variables {φ : β × δ → G} (hφ : continuous φ) [bilin : is_Z_bilin φ]
id                                  └────────┘             └────────┘
src                                 └────────┘             └────────┘
typ                                 └────────┘             └────────┘
doc                                  └────────┘
342  
343  include de df hφ bilin
344  
345  variables {W' : set G} (W'_nhd : W' ∈ 𝓝 (0 : G))
id                   └─┘                  
src                  └─┘                  
typ                  └─┘                  
doc                                        
346  include W'_nhd
347  
348  private lemma extend_Z_bilin_aux (x₀ : α) (y₁ : δ) :
id                                                  
typ                                                 
349    ∃ U₂ ∈ comap e (𝓝 x₀), ∀ x x' ∈ U₂, φ (x' - x, y₁) ∈ W' :=
id      └┘   └───┘    └┘     └┘   └┘   └┘    └┘   └┘
src          └───┘                                  
typ     └┘   └───┘    └┘     └┘   └┘   └┘    └┘   └┘
doc           └───┘    
350  begin
st   └─────
351    let Nx := 𝓝 x₀,
id                └┘
src    └────────┘
typ    └────────┘└┘
doc    └────────┘
txt    └────────┘ 
par    └────────┘ 
pid    └────┘└─┘ 
st   ───────────────┘└─
352    let ee := λ u : β × β, (e u.1, e u.2),
id                                 
src    └────────┘ └───┘  └┘  └──┘  └─┘
typ    └────────┘ └───┘ └┘  └──┘ └─┘
doc    └────────┘ └───┘   └┘   └──┘  └─┘
txt    └────────┘ └───┘   └┘   └──┘  └─┘
par    └────────┘ └───┘   └┘   └──┘  └─┘
pid    └────┘└─┘ └───┘   └┘   └──┘  └─┘
st   ──────────────────────────────────────┘└─
353  
st   
354    have lim1 : tendsto (λ a : β × β, (a.2 - a.1, y₁)) (filter.prod (comap e Nx) (comap e Nx)) (𝓝 (0, y₁)),
id                 └─────┘                               └─────────┘               └───┘  └┘         └┘
src    └──────────┘└─────┘  └───┘   └┘  └─┘ └──┘  └─┘ └─────────┘         └┘ └───┘   └─┘  └─┘  └┘
typ    └──────────┘└─────┘  └───┘  └┘  └─┘ └──┘  └─┘ └─────────┘         └┘ └───┘└┘└─┘  └─┘└┘└┘
doc    └──────────┘└─────┘  └───┘   └┘  └─┘  └──┘  └─┘ └─────────┘         └┘ └───┘   └─┘   └─┘  └┘
txt    └──────────┘         └───┘   └┘  └─┘  └──┘  └─┘                     └┘         └─┘   └─┘  └┘
par    └──────────┘         └───┘   └┘  └─┘  └──┘  └─┘                     └┘         └─┘   └─┘  └┘
pid    └───────┘└─┘         └───┘   └┘  └─┘  └──┘  └─┘                     └┘         └─┘   └─┘  └┘
st   ───────────────────────────────────────────────────────────────────────────────────────────────────────┘└─
355    { have := tendsto.prod_mk (tendsto_sub_comap_self de x₀) (tendsto_const_nhds : tendsto (λ (p : β × β), y₁) (comap ee $ 𝓝 (x₀, x₀)) (𝓝 y₁)),
id               └─────────────┘  └────────────────────┘ └┘      └────────────────┘   └─────┘                     └───┘ └┘         └┘      └┘
src      └──────┘└─────────────┘ └────────────────────┘    └┘ └────────────────┘└─┘└─────┘  └────┘   └─┘  └┘ └───┘      └┘  └─┘    └┘
typ      └──────┘└─────────────┘ └────────────────────┘└┘  └┘ └────────────────┘└─┘└─────┘  └────┘  └─┘  └┘ └───┘└┘    └┘└┘└─┘  └┘└┘
doc      └──────┘                                          └┘                   └─┘└─────┘  └────┘   └─┘  └┘ └───┘       └┘  └─┘    └┘
txt      └──────┘                                          └┘                   └─┘         └────┘   └─┘  └┘             └┘  └─┘    └┘
par      └──────┘                                          └┘                   └─┘         └────┘   └─┘  └┘             └┘  └─┘    └┘
pid      └───┘└─┘                                          └┘                   └─┘         └────┘   └─┘  └┘             └┘  └─┘    └┘
st   ───┘└──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘└─
356      rw [nhds_prod_eq, prod_comap_comap_eq, ←nhds_prod_eq],
id           └──────────┘  └─────────────────┘   └──────────┘
src      └──┘└──────────┘└┘└─────────────────┘└─┘└──────────┘
typ      └──┘└──────────┘└┘└─────────────────┘└─┘└──────────┘
doc      └──┘            └┘                   └─┘            
txt      └──┘            └┘                   └─┘            
par      └──┘            └┘                   └─┘            
pid        └┘            └┘                   └─┘            
st   ───────────────────┘└───────────────────┘└─────────────┘└──
357      exact (this : _) },
id              └──┘
src      └────┘     └────┘
typ      └────┘ └──┘└────┘
doc      └────┘     └────┘
txt      └────┘     └────┘
par      └────┘     └────┘
pid                └───┘
st   ────────────────────┘└┘
358  
st   
359    have lim := tendsto.comp (is_Z_bilin.tendsto_zero_right hφ y₁) lim1,
id                 └──────────┘  └───────────────────────────┘ └┘ └┘  └──┘
src    └──────────┘└──────────┘ └───────────────────────────┘    └┘
typ    └──────────┘└──────────┘ └───────────────────────────┘└┘└┘└┘└──┘
doc    └──────────┘                                              └┘
txt    └──────────┘                                              └┘
par    └──────────┘                                              └┘
pid    └──────┘└─┘                                              └┘
st   ────────────────────────────────────────────────────────────────────┘└─
360    rw tendsto_prod_self_iff at lim,
id        └───────────────────┘
src    └─┘└───────────────────┘└─────┘
typ    └─┘└───────────────────┘└─────┘
doc    └─┘                     └─────┘
txt    └─┘                     └─────┘
par    └─┘                     └─────┘
pid                           └─────┘
st   ────────────────────────────────┘└─
361    exact lim W' W'_nhd,
id           └─┘ └┘ └────┘
src    └────┘└─┘  
typ    └────┘└─┘└┘└────┘
doc    └────┘└─┘  
txt    └────┘     
par    └────┘     
pid              
st   ────────────────────┘└─
362  end
st   ──┘
363  
364  private lemma extend_Z_bilin_key (x₀ : α) (y₀ : γ) :
id                                                  
typ                                                 
365    ∃ U ∈ comap e (𝓝 x₀), ∃ V ∈ comap f (𝓝 y₀),
id         └───┘    └┘      └───┘    └┘ 
src         └───┘              └───┘        
typ        └───┘    └┘      └───┘    └┘ 
doc          └───┘                └───┘    
366      ∀ x x' ∈ U, ∀ y y' ∈ V, φ (x', y') - φ (x, y) ∈ W' :=
id          └┘        └┘      └┘  └┘         └┘
src                                                 
typ         └┘        └┘      └┘  └┘         └┘
367  begin
st   └─────
368    let Nx := 𝓝 x₀,
id                └┘
src    └────────┘
typ    └────────┘└┘
doc    └────────┘
txt    └────────┘ 
par    └────────┘ 
pid    └────┘└─┘ 
st   ───────────────┘└─
369    let Ny := 𝓝 y₀,
id                 └┘
src    └────────┘ 
typ    └────────┘ └┘
doc    └────────┘ 
txt    └────────┘ 
par    └────────┘ 
pid    └────┘└─┘ 
st   ───────────────┘└─
370    let dp := dense_inducing.prod de df,
id               └─────────────────┘ └┘ └┘
src    └────────┘└─────────────────┘  
typ    └────────┘└─────────────────┘└┘└┘
doc    └────────┘└─────────────────┘  
txt    └────────┘                     
par    └────────┘                     
pid    └────┘└─┘                     
st   ────────────────────────────────────┘└─
371    let ee := λ u : β × β, (e u.1, e u.2),
id                                 
src    └────────┘ └───┘  └┘  └──┘  └─┘
typ    └────────┘ └───┘ └┘  └──┘ └─┘
doc    └────────┘ └───┘   └┘   └──┘  └─┘
txt    └────────┘ └───┘   └┘   └──┘  └─┘
par    └────────┘ └───┘   └┘   └──┘  └─┘
pid    └────┘└─┘ └───┘   └┘   └──┘  └─┘
st   ──────────────────────────────────────┘└─
372    let ff := λ u : δ × δ, (f u.1, f u.2),
id                                 
src    └────────┘ └───┘   └┘  └──┘  └─┘
typ    └────────┘ └───┘ └┘  └──┘ └─┘
doc    └────────┘ └───┘   └┘   └──┘  └─┘
txt    └────────┘ └───┘   └┘   └──┘  └─┘
par    └────────┘ └───┘   └┘   └──┘  └─┘
pid    └────┘└─┘ └───┘   └┘   └──┘  └─┘
st   ──────────────────────────────────────┘└─
373  
st   
374    have lim_φ : filter.tendsto φ (𝓝 (0, 0)) (𝓝 0),
id                  └────────────┘     
src    └───────────┘└────────────┘   └─────┘  └─┘
typ    └───────────┘└────────────┘  └─────┘  └─┘
doc    └───────────┘└────────────┘    └─────┘  └─┘
txt    └───────────┘                  └─────┘  └─┘
par    └───────────┘                  └─────┘  └─┘
pid    └────────┘└─┘                  └─────┘  └─┘
st   ───────────────────────────────────────────────┘└─
375    { have := hφ.tendsto (0, 0),
id               └────────┘ 
src      └──────┘└────────┘└───┘
typ      └──────┘└────────┘└───┘
doc      └──────┘           └───┘
txt      └──────┘           └───┘
par      └──────┘           └───┘
pid      └───┘└─┘           └───┘
st   ───┘└───────────────────────┘└─
376      rwa [is_Z_bilin.zero φ] at this },
id            └─────────────┘ 
src      └───┘└─────────────┘ └────────┘
typ      └───┘└─────────────┘└────────┘
doc      └───┘                └────────┘
txt      └───┘                └────────┘
par      └───┘                └────────┘
pid         └┘                └──────┘
st   ─────────────────────────┘└───────┘└┘
377  
st   
378    have lim_φ_sub_sub : tendsto (λ (p : (β × β) × (δ × δ)), φ (p.1.2 - p.1.1, p.2.2 - p.2.1))
id                          └─────┘                                  
src    └───────────────────┘└─────┘  └────┘    └┘     └──┘   └───┘ └────┘ └───┘  └──────
typ    └───────────────────┘└─────┘  └────┘   └┘   └──┘  └───┘ └────┘ └───┘  └──────
doc    └───────────────────┘└─────┘  └────┘    └┘     └──┘   └───┘  └────┘ └───┘  └──────
txt    └───────────────────┘         └────┘    └┘     └──┘   └───┘  └────┘ └───┘  └──────
par    └───────────────────┘         └────┘    └┘     └──┘   └───┘  └────┘ └───┘  └──────
pid    └────────────────┘└─┘         └────┘    └┘     └──┘   └───┘  └────┘ └───┘  └──────
st   ─────────────────────────────────────────────────────────────────────────────────────────────
379      (filter.prod (comap ee $ 𝓝 (x₀, x₀)) (comap ff $ 𝓝 (y₀, y₀))) (𝓝 0),
id        └─────────┘        └┘          └┘    └───┘ └┘         └┘
src  ───┘ └─────────┘             └┘  └─┘ └───┘      └┘  └──┘  └─┘
typ  ───┘ └─────────┘      └┘     └┘└┘└─┘ └───┘└┘    └┘└┘└──┘  └─┘
doc  ───┘ └─────────┘             └┘  └─┘ └───┘       └┘  └──┘  └─┘
txt  ───┘                         └┘  └─┘             └┘  └──┘  └─┘
par  ───┘                         └┘  └─┘             └┘  └──┘  └─┘
pid  ───┘                         └┘  └─┘             └┘  └──┘  └─┘
st   ──────────────────────────────────────────────────────────────────────┘└─
380    { have lim_sub_sub :  tendsto (λ (p : (β × β) × δ × δ), (p.1.2 - p.1.1, p.2.2 - p.2.1))
id                           └─────┘                      
src      └──────────────────┘└─────┘  └────┘    └┘    └─┘  └───┘  └────┘ └───┘  └──────
typ      └──────────────────┘└─────┘  └────┘   └┘   └─┘  └───┘  └────┘ └───┘  └──────
doc      └──────────────────┘└─────┘  └────┘    └┘    └─┘  └───┘  └────┘ └───┘  └──────
txt      └──────────────────┘         └────┘    └┘    └─┘  └───┘  └────┘ └───┘  └──────
par      └──────────────────┘         └────┘    └┘    └─┘  └───┘  └────┘ └───┘  └──────
pid      └──────────────┘└──┘         └────┘    └┘    └─┘  └───┘  └────┘ └───┘  └──────
st   ───┘└─────────────────────────────────────────────────────────────────────────────────────
381        (filter.prod (comap ee (𝓝 (x₀, x₀))) (comap ff (𝓝 (y₀, y₀)))) (filter.prod (𝓝 0) (𝓝 0)),
id                             └┘         └┘     └───┘ └┘        └┘      └─────────┘
src  ─────┘                         └┘  └──┘ └───┘      └┘  └───┘ └─────────┘  └──┘  └──┘
typ  ─────┘                  └┘     └┘└┘└──┘ └───┘└┘    └┘└┘└───┘ └─────────┘  └──┘  └──┘
doc  ─────┘                         └┘  └──┘ └───┘       └┘  └───┘ └─────────┘  └──┘  └──┘
txt  ─────┘                         └┘  └──┘             └┘  └───┘              └──┘  └──┘
par  ─────┘                         └┘  └──┘             └┘  └───┘              └──┘  └──┘
pid  ─────┘                         └┘  └──┘             └┘  └───┘              └──┘  └──┘
st   ────────────────────────────────────────────────────────────────────────────────────────────┘└─
382      { have := filter.prod_mono (tendsto_sub_comap_self de x₀) (tendsto_sub_comap_self df y₀),
id                 └──────────────┘                         └┘ └┘   └────────────────────┘ └┘ └┘
src        └──────┘└──────────────┘                           └┘ └────────────────────┘    
typ        └──────┘└──────────────┘                       └┘└┘└┘ └────────────────────┘└┘└┘
doc        └──────┘                                           └┘                           
txt        └──────┘                                           └┘                           
par        └──────┘                                           └┘                           
pid        └───┘└─┘                                           └┘                           
st   ─────┘└────────────────────────────────────────────────────────────────────────────────────┘└─
383        rwa prod_map_map_eq at this },
id             └─────────────┘
src        └──┘└─────────────┘└───────┘
typ        └──┘└─────────────┘└───────┘
doc        └──┘               └───────┘
txt        └──┘               └───────┘
par        └──┘               └───────┘
pid                          └──────┘
st   ─────────────────────────────────┘└┘
384      rw ← nhds_prod_eq at lim_sub_sub,
id            └──────────┘
src      └───┘└──────────┘└─────────────┘
typ      └───┘└──────────┘└─────────────┘
doc      └───┘            └─────────────┘
txt      └───┘            └─────────────┘
par      └───┘            └─────────────┘
pid        └─┘            └─────────────┘
st   ───────────────────────────────────┘└─
385      exact tendsto.comp lim_φ lim_sub_sub },
id             └──────────┘ └───┘ └─────────┘
src      └────┘└──────────┘                
typ      └────┘└──────────┘└───┘└─────────┘
doc      └────┘                            
txt      └────┘                            
par      └────┘                            
pid                                       
st   ────────────────────────────────────────┘└┘
386  
st   
387    rcases exists_nhds_quarter W'_nhd with ⟨W, W_nhd, W4⟩,
id            └─────────────────┘ └────┘
src    └─────┘└─────────────────┘      └──────────────────┘
typ    └─────┘└─────────────────┘└────┘└──────────────────┘
doc    └─────┘                         └──────────────────┘
txt    └─────┘                         └──────────────────┘
par    └─────┘                         └──────────────────┘
pid                                   └──────────────────┘
st   ──────────────────────────────────────────────────────┘└─
388  
st   
389    have : ∃ U₁ ∈ comap e (𝓝 x₀), ∃ V₁ ∈ comap f (𝓝 y₀),
id                            └┘         └───┘     └┘
src    └─────┘└────┘           └────┘└───┘      
typ    └─────┘└────┘       └┘ └────┘└───┘  └┘ 
doc    └─────┘ └────┘            └────┘└───┘      
txt    └─────┘ └────┘            └────┘           
par    └─────┘ └────┘            └────┘           
pid    └───┘└┘ └────┘            └────┘           
st   ───────────────────────────────────────────────────────
390      ∀ x x' ∈ U₁, ∀ y y' ∈ V₁,  φ (x'-x, y'-y) ∈ W,
id                                                 
src  ───┘ └──────┘    └──────┘   └┘     └┘    └┘ 
typ  ───┘ └──────┘    └──────┘   └┘    └┘    └┘ 
doc  ───┘ └──────┘    └──────┘   └┘      └┘    └┘ 
txt  ───┘ └──────┘    └──────┘   └┘      └┘    └┘ 
par  ───┘ └──────┘    └──────┘   └┘      └┘    └┘ 
pid  ───┘ └──────┘    └──────┘   └┘      └┘    └┘ 
st   ────────────────────────────────────────────────┘└─
391    { have := tendsto_prod_iff.1 lim_φ_sub_sub W W_nhd,
id               └──────────────┘   └───────────┘  └───┘
src      └──────┘└──────────────┘└─┘              
typ      └──────┘└──────────────┘└─┘└───────────┘└───┘
doc      └──────┘                └─┘              
txt      └──────┘                └─┘              
par      └──────┘                └─┘              
pid      └───┘└─┘                └─┘              
st   ───┘└──────────────────────────────────────────────┘└─
392      repeat { rw [nhds_prod_eq, ←prod_comap_comap_eq] at this },
id                    └──────────┘   └─────────────────┘
src      └───────┘└──┘└──────────┘└─┘└─────────────────┘└────────┘
typ      └───────┘└──┘└──────────┘└─┘└─────────────────┘└────────┘
doc      └───────┘└──┘            └─┘                   └────────┘
txt      └───────┘└──┘            └─┘                   └────────┘
par      └───────┘└──┘            └─┘                   └────────┘
pid            └─────┘            └─┘                   └─────────┘
st   ────────────────────────────┘└────────────────────┘└───────┘└┘
393      rcases this with ⟨U, U_in, V, V_in, H⟩,
id              └──┘
src      └─────┘    └─────────────────────────┘
typ      └─────┘└──┘└─────────────────────────┘
doc      └─────┘    └─────────────────────────┘
txt      └─────┘    └─────────────────────────┘
par      └─────┘    └─────────────────────────┘
pid                └─────────────────────────┘
st   ─────────────────────────────────────────┘└─
394      rw [mem_prod_same_iff] at U_in V_in,
id           └───────────────┘
src      └──┘└───────────────┘└────────────┘
typ      └──┘└───────────────┘└────────────┘
doc      └──┘                 └────────────┘
txt      └──┘                 └────────────┘
par      └──┘                 └────────────┘
pid        └┘                 └───────────┘
st   ────────────────────────┘└───────────┘└─
395      rcases U_in with ⟨U₁, U₁_in, HU₁⟩,
id              └──┘
src      └─────┘    └────────────────────┘
typ      └─────┘└──┘└────────────────────┘
doc      └─────┘    └────────────────────┘
txt      └─────┘    └────────────────────┘
par      └─────┘    └────────────────────┘
pid                └────────────────────┘
st   ────────────────────────────────────┘└─
396      rcases V_in with ⟨V₁, V₁_in, HV₁⟩,
id              └──┘
src      └─────┘    └────────────────────┘
typ      └─────┘└──┘└────────────────────┘
doc      └─────┘    └────────────────────┘
txt      └─────┘    └────────────────────┘
par      └─────┘    └────────────────────┘
pid                └────────────────────┘
st   ────────────────────────────────────┘└─
397      existsi [U₁, U₁_in, V₁, V₁_in],
id                └┘  └───┘  └┘  └───┘
src      └───────┘  └┘     └┘  └┘     
typ      └───────┘└┘└┘└───┘└┘└┘└┘└───┘
doc      └───────┘  └┘     └┘  └┘     
txt      └───────┘  └┘     └┘  └┘     
par      └───────┘  └┘     └┘  └┘     
pid             └┘  └┘     └┘  └┘     
st   ─────────────────────────────────┘└─
398      intros x x' x_in x'_in y y' y_in y'_in,
src      └────────────────────────────────────┘
typ      └────────────────────────────────────┘
doc      └────────────────────────────────────┘
txt      └────────────────────────────────────┘
par      └────────────────────────────────────┘
pid            └──────────────────────────────┘
st   ─────────────────────────────────────────┘└─
399      exact H _ _ (HU₁ (mk_mem_prod x_in x'_in)) (HV₁ (mk_mem_prod y_in y'_in)) },
id                   └─┘              └──┘ └───┘    └─┘  └─────────┘ └──┘ └───┘
src      └────┘ └───┘                         └─┘     └─────────┘         └─┘
typ      └────┘└───┘ └─┘            └──┘└───┘└─┘ └─┘ └─────────┘└──┘└───┘└─┘
doc      └────┘ └───┘                         └─┘                         └─┘
txt      └────┘ └───┘                         └─┘                         └─┘
par      └────┘ └───┘                         └─┘                         └─┘
pid            └───┘                         └─┘                         └┘
st   ─────────────────────────────────────────────────────────────────────────────┘└┘
400    rcases this with ⟨U₁, U₁_nhd, V₁, V₁_nhd, H⟩,
id            └──┘
src    └─────┘    └───────────────────────────────┘
typ    └─────┘└──┘└───────────────────────────────┘
doc    └─────┘    └───────────────────────────────┘
txt    └─────┘    └───────────────────────────────┘
par    └─────┘    └───────────────────────────────┘
pid              └───────────────────────────────┘
st   ─────────────────────────────────────────────┘└─
401  
st   
402    obtain ⟨x₁, x₁_in⟩ : U₁.nonempty :=
id                          └─────────┘
src    └───────────────────┘└─────────┘└───
typ    └───────────────────┘└─────────┘└───
doc    └───────────────────┘└─────────┘└───
txt    └───────────────────┘           └───
par    └───────────────────┘           └───
pid          └─────────────┘           └───
st   ──────────────────────────────────────
403      (forall_sets_nonempty_iff_ne_bot.2 de.comap_nhds_ne_bot U₁ U₁_nhd),
id        └─────────────────────────────┘   └──────────────────┘ └┘ └────┘
src  ───┘ └─────────────────────────────┘└─┘└──────────────────┘        
typ  ───┘ └─────────────────────────────┘└─┘└──────────────────┘└┘└────┘
doc  ───┘                                └─┘                            
txt  ───┘                                └─┘                            
par  ───┘                                └─┘                            
pid  ───┘                                └─┘                            
st   ─────────────────────────────────────────────────────────────────────┘└─
404    obtain ⟨y₁, y₁_in⟩ : V₁.nonempty :=
id                          └─────────┘
src    └───────────────────┘└─────────┘└───
typ    └───────────────────┘└─────────┘└───
doc    └───────────────────┘└─────────┘└───
txt    └───────────────────┘           └───
par    └───────────────────┘           └───
pid          └─────────────┘           └───
st   ──────────────────────────────────────
405      (forall_sets_nonempty_iff_ne_bot.2 df.comap_nhds_ne_bot V₁ V₁_nhd),
id        └─────────────────────────────┘   └──────────────────┘ └┘ └────┘
src  ───┘ └─────────────────────────────┘└─┘└──────────────────┘        
typ  ───┘ └─────────────────────────────┘└─┘└──────────────────┘└┘└────┘
doc  ───┘                                └─┘                            
txt  ───┘                                └─┘                            
par  ───┘                                └─┘                            
pid  ───┘                                └─┘                            
st   ─────────────────────────────────────────────────────────────────────┘└─
406  
st   
407    rcases (extend_Z_bilin_aux de df hφ W_nhd x₀ y₁) with ⟨U₂, U₂_nhd, HU⟩,
id             └────────────────┘ └┘ └┘ └┘ └───┘ └┘ └┘
src    └─────┘ └────────────────┘               └─────────────────────┘
typ    └─────┘ └────────────────┘└┘└┘└┘└───┘└┘└┘└─────────────────────┘
doc    └─────┘                                  └─────────────────────┘
txt    └─────┘                                  └─────────────────────┘
par    └─────┘                                  └─────────────────────┘
pid                                            └─────────────────────┘
st   ───────────────────────────────────────────────────────────────────────┘└─
408    rcases (extend_Z_bilin_aux df de (hφ.comp continuous_swap) W_nhd y₀ x₁) with ⟨V₂, V₂_nhd, HV⟩,
id             └────────────────┘ └┘ └┘  └─────┘ └─────────────┘  └───┘ └┘ └┘
src    └─────┘ └────────────────┘     └─────┘└─────────────┘└┘         └─────────────────────┘
typ    └─────┘ └────────────────┘└┘└┘ └─────┘└─────────────┘└┘└───┘└┘└┘└─────────────────────┘
doc    └─────┘                                              └┘         └─────────────────────┘
txt    └─────┘                                              └┘         └─────────────────────┘
par    └─────┘                                              └┘         └─────────────────────┘
pid                                                        └┘         └─────────────────────┘
st   ──────────────────────────────────────────────────────────────────────────────────────────────┘└─
409  
st   
410    existsi [U₁ ∩ U₂, inter_mem_sets U₁_nhd U₂_nhd,
id              └┘  └┘  └────────────┘ └────┘ └────┘
src    └───────┘    └┘└────────────┘            └─
typ    └───────┘└┘└┘└┘└────────────┘└────┘└────┘└─
doc    └───────┘     └┘                          └─
txt    └───────┘     └┘                          └─
par    └───────┘     └┘                          └─
pid           └┘     └┘                          └─
st   ──────────────────────────────────────────────────
411              V₁ ∩ V₂, inter_mem_sets V₁_nhd V₂_nhd],
id               └┘   └┘  └────────────┘ └────┘ └────┘
src  ───────────┘     └┘└────────────┘            
typ  ───────────┘└┘ └┘└┘└────────────┘└────┘└────┘
doc  ───────────┘     └┘                          
txt  ───────────┘     └┘                          
par  ───────────┘     └┘                          
pid  ───────────┘     └┘                          
st   ─────────────────────────────────────────────────┘└─
412  
st   
413    rintros x x' ⟨xU₁, xU₂⟩ ⟨x'U₁, x'U₂⟩ y y' ⟨yV₁, yV₂⟩ ⟨y'V₁, y'V₂⟩,
src    └───────────────────────────────────────────────────────────────┘
typ    └───────────────────────────────────────────────────────────────┘
doc    └───────────────────────────────────────────────────────────────┘
txt    └───────────────────────────────────────────────────────────────┘
par    └───────────────────────────────────────────────────────────────┘
pid           └────────────────────────────────────────────────────────┘
st   ──────────────────────────────────────────────────────────────────┘└─
414    have key_formula : φ(x', y') - φ(x, y) = φ(x' - x, y₁) + φ(x' - x, y' - y₁) + φ(x₁, y' - y) + φ(x - x₁, y' - y),
id                                                              └┘           └┘                       └┘  └┘   
src    └─────────────────┘    └┘  └┘    └┘ └┘      └┘  └┘      └┘     └┘     └┘    └┘      └┘    
typ    └─────────────────┘    └┘  └┘    └┘ └┘      └┘  └┘  └┘  └┘   └┘└┘     └┘    └┘  └┘└┘└┘ 
doc    └─────────────────┘    └┘  └┘    └┘ └┘       └┘  └┘       └┘     └┘     └┘    └┘       └┘    
txt    └─────────────────┘    └┘  └┘    └┘ └┘       └┘  └┘       └┘     └┘     └┘    └┘       └┘    
par    └─────────────────┘    └┘  └┘    └┘ └┘       └┘  └┘       └┘     └┘     └┘    └┘       └┘    
pid    └──────────────┘└─┘    └┘  └┘    └┘ └┘       └┘  └┘       └┘     └┘     └┘    └┘       └┘    
st   ────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘└─
415    { repeat { rw is_Z_bilin.sub_left φ },
id                   └─────────────────┘ 
src      └───────┘└─┘└─────────────────┘ 
typ      └───────┘└─┘└─────────────────┘
doc      └───────┘└─┘                    
txt      └───────┘└─┘                    
par      └───────┘└─┘                    
pid            └────┘                    └┘
st   ───┘└────────────────────────────────┘└┘
416      repeat { rw is_Z_bilin.sub_right φ },
id                   └──────────────────┘ 
src      └───────┘└─┘└──────────────────┘ 
typ      └───────┘└─┘└──────────────────┘
doc      └───────┘└─┘                     
txt      └───────┘└─┘                     
par      └───────┘└─┘                     
pid            └────┘                     └┘
st   ──────────────────────────────────────┘└┘
417      apply eq_of_sub_eq_zero,
id             └───────────────┘
src      └────┘└───────────────┘
typ      └────┘└───────────────┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ──────────────────────────┘└─
418      simp },
src      └───┘
typ      └───┘
doc      └───┘
txt      └───┘
par      └───┘
pid          
st   ────────┘└┘
419    rw key_formula,
id        └─────────┘
src    └─┘
typ    └─┘└─────────┘
doc    └─┘
txt    └─┘
par    └─┘
pid      
st   ───────────────┘└─
420    have h₁ := HU x x' xU₂ x'U₂,
id                └┘  └┘ └─┘ └──┘
src    └─────────┘        
typ    └─────────┘└┘└┘└─┘└──┘
doc    └─────────┘        
txt    └─────────┘        
par    └─────────┘        
pid    └─────┘└─┘        
st   ────────────────────────────┘└─
421    have h₂ := H x x' xU₁ x'U₁ y₁ y' y₁_in y'V₁,
id                  └┘ └─┘ └──┘ └┘ └┘ └───┘ └──┘
src    └─────────┘                    
typ    └─────────┘└┘└─┘└──┘└┘└┘└───┘└──┘
doc    └─────────┘                    
txt    └─────────┘                    
par    └─────────┘                    
pid    └─────┘└─┘                    
st   ────────────────────────────────────────────┘└─
422    have h₃ := HV y y' yV₂ y'V₂,
id                └┘  └┘ └─┘ └──┘
src    └─────────┘        
typ    └─────────┘└┘└┘└─┘└──┘
doc    └─────────┘        
txt    └─────────┘        
par    └─────────┘        
pid    └─────┘└─┘        
st   ────────────────────────────┘└─
423    have h₄ := H x₁ x x₁_in xU₁ y y' yV₁ y'V₁,
id                 └┘  └───┘ └─┘  └┘ └─┘ └──┘
src    └─────────┘                  
typ    └─────────┘└┘└───┘└─┘└┘└─┘└──┘
doc    └─────────┘                  
txt    └─────────┘                  
par    └─────────┘                  
pid    └─────┘└─┘                  
st   ──────────────────────────────────────────┘└─
424  
st   
425    exact W4 h₁ h₂ h₃ h₄
id           └┘ └┘ └┘ └┘ └┘
src    └────┘          
typ    └────┘└┘└┘└┘└┘└┘
doc    └────┘          
txt    └────┘          
par    └────┘          
pid                   
st   ──────────────────────┘
426  end
st   └─┘
427  
428  omit W'_nhd
429  
430  open dense_inducing
431  
432  /-- Bourbaki GT III.6.5 Theorem I:
433  ℤ-bilinear continuous maps from dense images into a complete Hausdorff group extend by continuity.
434  Note: Bourbaki assumes that α and β are also complete Hausdorff, but this is not necessary. -/
435  theorem extend_Z_bilin  : continuous (extend (de.prod df) φ) :=
id                             └────────┘  └────┘  └┘└───┘ └┘  
src                            └────────┘  └────┘    └───┘
typ                            └────────┘  └────┘  └┘└───┘ └┘  
doc                            └────────┘  └────┘    └───┘
436  begin
st   └─────
437    refine continuous_extend_of_cauchy _ _,
id            └─────────────────────────┘
src    └─────┘└─────────────────────────┘└──┘
typ    └─────┘└─────────────────────────┘└──┘
doc    └─────┘                           └──┘
txt    └─────┘                           └──┘
par    └─────┘                           └──┘
pid                                     └──┘
st   ───────────────────────────────────────┘└─
438    rintro ⟨x₀, y₀⟩,
src    └─────────────┘
typ    └─────────────┘
doc    └─────────────┘
txt    └─────────────┘
par    └─────────────┘
pid          └───────┘
st   ────────────────┘└─
439    split,
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
st   ──────┘└─
440    { apply map_ne_bot,
id             └────────┘
src      └────┘└────────┘
typ      └────┘└────────┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ───┘└──────────────┘└─
441      apply comap_ne_bot,
id             └──────────┘
src      └────┘└──────────┘
typ      └────┘└──────────┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ─────────────────────┘└─
442  
st   
443      intros U h,
src      └────────┘
typ      └────────┘
doc      └────────┘
txt      └────────┘
par      └────────┘
pid            └──┘
st   ─────────────┘└─
444      rcases mem_closure_iff_nhds.1 ((de.prod df).dense (x₀, y₀)) U h with ⟨x, x_in, ⟨z, z_x⟩⟩,
id              └──────────────────┘     └─────┘ └┘        └┘  └┘    
src      └─────┘└──────────────────┘└─┘  └─────┘  └──────┘  └┘  └─┘  └───────────────────────┘
typ      └─────┘└──────────────────┘└─┘  └─────┘└┘└──────┘└┘└┘└┘└─┘└───────────────────────┘
doc      └─────┘                    └─┘  └─────┘  └──────┘   └┘  └─┘  └───────────────────────┘
txt      └─────┘                    └─┘           └──────┘   └┘  └─┘  └───────────────────────┘
par      └─────┘                    └─┘           └──────┘   └┘  └─┘  └───────────────────────┘
pid                                └─┘           └──────┘   └┘  └─┘  └───────────────────────┘
st   ───────────────────────────────────────────────────────────────────────────────────────────┘└─
445      existsi z,
id               
src      └──────┘
typ      └──────┘
doc      └──────┘
txt      └──────┘
par      └──────┘
pid             
st   ────────────┘└─
446      cc },
src      └─┘
typ      └─┘
doc      └─┘
txt      └─┘
par      └─┘
pid        
st   ──────┘└┘
447    { suffices : map (λ (p : (β × δ) × (β × δ)), φ p.2 - φ p.1)
id                  └─┘                                  
src      └─────────┘└─┘  └────┘   └┘     └──┘  └─┘  └───
typ      └─────────┘└─┘  └────┘   └┘    └──┘  └─┘ └───
doc      └─────────┘└─┘  └────┘    └┘     └──┘  └─┘   └───
txt      └─────────┘     └────┘    └┘     └──┘  └─┘   └───
par      └─────────┘     └────┘    └┘     └──┘  └─┘   └───
pid      └───────┘└┘     └────┘    └┘     └──┘  └─┘   └───
st   ──────────────────────────────────────────────────────────────
448        (comap (λ (p : (β × δ) × β × δ), ((e p.1.1, f p.1.2), (e p.2.1, f p.2.2)))
id          └───┘                                                       
src  ─────┘ └───┘  └────┘    └┘    └─┘    └────┘  └─────┘   └────┘  └───────
typ  ─────┘ └───┘  └────┘    └┘  └─┘    └────┘  └─────┘  └────┘ └───────
doc  ─────┘ └───┘  └────┘    └┘    └─┘    └────┘  └─────┘   └────┘  └───────
txt  ─────┘        └────┘    └┘    └─┘    └────┘  └─────┘   └────┘  └───────
par  ─────┘        └────┘    └┘    └─┘    └────┘  └─────┘   └────┘  └───────
pid  ─────┘        └────┘    └┘    └─┘    └────┘  └─────┘   └────┘  └───────
st   ─────────────────────────────────────────────────────────────────────────────────
449           (filter.prod (𝓝 (x₀, y₀)) (𝓝 (x₀, y₀)))) ≤ 𝓝 0,
id             └─────────┘                └┘  └┘     
src  ────────┘ └─────────┘    └┘  └─┘    └┘  └───┘ └┘
typ  ────────┘ └─────────┘    └┘  └─┘  └┘└┘└┘└───┘ └┘
doc  ────────┘ └─────────┘    └┘  └─┘     └┘  └───┘  └┘
txt  ────────┘                 └┘  └─┘     └┘  └───┘  └┘
par  ────────┘                 └┘  └─┘     └┘  └───┘  └┘
pid  ────────┘                 └┘  └─┘     └┘  └───┘  
st   ──────────────────────────────────────────────────────┘
450      by rwa [uniformity_eq_comap_nhds_zero G, prod_map_map_eq, ←map_le_iff_le_comap, filter.map_map,
id               └───────────────────────────┘   └─────────────┘   └─────────────────┘  └────────────┘
src         └───┘└───────────────────────────┘ └┘└─────────────┘└─┘└─────────────────┘└┘└────────────┘└─
typ         └───┘└───────────────────────────┘└┘└─────────────┘└─┘└─────────────────┘└┘└────────────┘└─
doc         └───┘                              └┘               └─┘                   └┘              └─
txt         └───┘                              └┘               └─┘                   └┘              └─
par         └───┘                              └┘               └─┘                   └┘              └─
pid            └┘                              └┘               └─┘                   └┘              └─
st               └─────────────────────────────┘└───────────────┘└────────────────────┘└──────────────┘└─
451          prod_comap_comap_eq],
id           └─────────────────┘
src  ───────┘└─────────────────┘
typ  ───────┘└─────────────────┘
doc  ───────┘                   
txt  ───────┘                   
par  ───────┘                   
pid  ───────┘                   
st   ──────────────────────────┘└─
452  
st   
453      intros W' W'_nhd,
src      └──────────────┘
typ      └──────────────┘
doc      └──────────────┘
txt      └──────────────┘
par      └──────────────┘
pid            └────────┘
st   ───────────────────┘└─
454  
st   
455      have key := extend_Z_bilin_key de df hφ W'_nhd x₀ y₀,
id                   └────────────────┘ └┘ └┘ └┘ └────┘ └┘ └┘
src      └──────────┘└────────────────┘              
typ      └──────────┘└────────────────┘└┘└┘└┘└────┘└┘└┘
doc      └──────────┘                                
txt      └──────────┘                                
par      └──────────┘                                
pid      └──────┘└─┘                                
st   ───────────────────────────────────────────────────────┘└─
456      rcases key with ⟨U, U_nhd, V, V_nhd, h⟩,
id              └─┘
src      └─────┘   └───────────────────────────┘
typ      └─────┘└─┘└───────────────────────────┘
doc      └─────┘   └───────────────────────────┘
txt      └─────┘   └───────────────────────────┘
par      └─────┘   └───────────────────────────┘
pid               └───────────────────────────┘
st   ──────────────────────────────────────────┘└─
457      rw mem_comap_sets at U_nhd,
id          └────────────┘
src      └─┘└────────────┘└───────┘
typ      └─┘└────────────┘└───────┘
doc      └─┘              └───────┘
txt      └─┘              └───────┘
par      └─┘              └───────┘
pid                      └───────┘
st   ─────────────────────────────┘└─
458      rcases U_nhd with ⟨U', U'_nhd, U'_sub⟩,
id              └───┘
src      └─────┘     └────────────────────────┘
typ      └─────┘└───┘└────────────────────────┘
doc      └─────┘     └────────────────────────┘
txt      └─────┘     └────────────────────────┘
par      └─────┘     └────────────────────────┘
pid                 └────────────────────────┘
st   ─────────────────────────────────────────┘└─
459      rw mem_comap_sets at V_nhd,
id          └────────────┘
src      └─┘└────────────┘└───────┘
typ      └─┘└────────────┘└───────┘
doc      └─┘              └───────┘
txt      └─┘              └───────┘
par      └─┘              └───────┘
pid                      └───────┘
st   ─────────────────────────────┘└─
460      rcases V_nhd with ⟨V', V'_nhd, V'_sub⟩,
id              └───┘
src      └─────┘     └────────────────────────┘
typ      └─────┘└───┘└────────────────────────┘
doc      └─────┘     └────────────────────────┘
txt      └─────┘     └────────────────────────┘
par      └─────┘     └────────────────────────┘
pid                 └────────────────────────┘
st   ─────────────────────────────────────────┘└─
461  
st   
462      rw [mem_map, mem_comap_sets, nhds_prod_eq],
id           └─────┘  └────────────┘  └──────────┘
src      └──┘└─────┘└┘└────────────┘└┘└──────────┘
typ      └──┘└─────┘└┘└────────────┘└┘└──────────┘
doc      └──┘       └┘              └┘            
txt      └──┘       └┘              └┘            
par      └──┘       └┘              └┘            
pid        └┘       └┘              └┘            
st   ──────────────┘└──────────────┘└────────────┘└──
463      existsi set.prod (set.prod U' V') (set.prod U' V'),
id                                          └──────┘ └┘ └┘
src      └──────┘                     └┘ └──────┘    
typ      └──────┘                     └┘ └──────┘└┘└┘
doc      └──────┘                     └┘ └──────┘    
txt      └──────┘                     └┘             
par      └──────┘                     └┘             
pid                                  └┘             
st   ─────────────────────────────────────────────────────┘└─
464      rw mem_prod_same_iff,
id          └───────────────┘
src      └─┘└───────────────┘
typ      └─┘└───────────────┘
doc      └─┘
txt      └─┘
par      └─┘
pid        
st   ───────────────────────┘└─
465  
st   
466      simp only [exists_prop],
id                  └─────────┘
src      └─────────┘└─────────┘
typ      └─────────┘└─────────┘
doc      └─────────┘           
txt      └─────────┘           
par      └─────────┘           
pid          └──┘└┘           
st   ──────────────────────────┘└─
467      split,
src      └───┘
typ      └───┘
doc      └───┘
txt      └───┘
par      └───┘
st   ────────┘└─
468      { change U' ∈ 𝓝 x₀ at U'_nhd,
id                └┘    └┘
src        └─────┘     └────────┘
typ        └─────┘└┘ └┘└────────┘
doc        └─────┘      └────────┘
txt        └─────┘      └────────┘
par        └─────┘      └────────┘
pid                    └───────┘
st   ─────┘└────────────────────────┘└─
469        change V' ∈ 𝓝 y₀ at V'_nhd,
id                └┘     └┘
src        └─────┘      └────────┘
typ        └─────┘└┘  └┘└────────┘
doc        └─────┘      └────────┘
txt        └─────┘      └────────┘
par        └─────┘      └────────┘
pid                    └───────┘
st   ───────────────────────────────┘└─
470        have := prod_mem_prod U'_nhd V'_nhd,
id                 └───────────┘ └────┘ └────┘
src        └──────┘└───────────┘      
typ        └──────┘└───────────┘└────┘└────┘
doc        └──────┘                   
txt        └──────┘                   
par        └──────┘                   
pid        └───┘└─┘                   
st   ────────────────────────────────────────┘└─
471        tauto },
src        └────┘
typ        └────┘
doc        └────┘
txt        └────┘
par        └────┘
pid             
st   ───────────┘└┘
472      { intros p h',
src        └─────────┘
typ        └─────────┘
doc        └─────────┘
txt        └─────────┘
par        └─────────┘
pid              └───┘
st   ────────────────┘└─
473        simp only [set.mem_preimage, set.prod_mk_mem_set_prod_eq] at h',
id                    └──────────────┘  └─────────────────────────┘
src        └─────────┘└──────────────┘└┘└─────────────────────────┘└─────┘
typ        └─────────┘└──────────────┘└┘└─────────────────────────┘└─────┘
doc        └─────────┘                └┘                           └─────┘
txt        └─────────┘                └┘                           └─────┘
par        └─────────┘                └┘                           └─────┘
pid            └──┘└┘                └┘                           └───┘
st   ────────────────────────────────────────────────────────────────────┘└─
474        rcases p with ⟨⟨x, y⟩, ⟨x', y'⟩⟩,
id                
src        └─────┘ └──────────────────────┘
typ        └─────┘└──────────────────────┘
doc        └─────┘ └──────────────────────┘
txt        └─────┘ └──────────────────────┘
par        └─────┘ └──────────────────────┘
pid               └──────────────────────┘
st   ─────────────────────────────────────┘└─
475        apply h ; tauto } }
src        └────┘   └────┘
typ        └────┘   └────┘
doc        └────┘   └────┘
txt        └────┘   └────┘
par        └────┘   └────┘
pid                     
st   ─────────────────────┘└───
476  end
st   ──┘
477  end dense_inducing